速報:アリストテレスの消費者版がプットナムを打ち破り、@leanproverで10/12の問題を解決し正式に検証。 アマチュア数学者である@namrata_anand2、アリストテレスの消費者向け版を早期に公に発表したことにおめでとうございます。アリストテレスはそれらを朝食に食べ、10/12を完全に自律的に解いたようです。 現在ファイルを調査中で、詳細は後ほど共有しますが、今指摘しておきたい有益な点が2つあります。 ▪️これらは2025年のパットナム問題に対する初めての完全に形式的に公開された解決策のようです。 ▪️これらはすべて、最近公開された自然言語インターフェースを使い、アリストテレスに自然言語で質問を与え、それをLean4文に自己形式化し、人間が関与しない状態で証明を完了するものでした。これまではアリストテレスの最先端の定理証明能力に注目してきましたが、現在は自己形式化にもかなり対応できるようになっています。 私たちはAIと数学の新たな夜明けに突入しています。ゆっくりと。。。そして一気に!