私は個人的に一線を越えてしまい、少し感嘆しています。 これは私にとって初めての完全自動化されたLLMによる自動形式化された新しい数学定理の証明です。 問題を説明します:3つの回転円があり、それぞれ6つの位置があり、合計6点で交差しています。 それらが生み出す運動群が完全な対称群であることを証明するS_{12}。 これは、Amanita Designのゲーム『Machinarium』の素敵なパズルで最初に気づいた問題です。 この課題は非常に難しくはありませんが、どうやら2つの証明があるようです。 1. 全転置を表すために共役クラスをブルートフォースで探索する(これは何年も前にやったが、公開はしていない)。 2. LLM生成の証明(この場合はGPT-5-Proが約3か月前に作成したもの)、または実際には2つの証明で、どちらも原始群に関するジョーダンの定理(またはさらに直接的な密接に関連する変種)を見事に用いています。( 今夜まで私が欠けていたのは、この証明を自動形式化するツールでした。 @HarmonicMathのおかげで、彼らの素晴らしいソフトウェア、アリストテレスにアクセスできました。まとめると、私がやったことは以下の通りです: A. LLMで証明を自動生成し(複数回実行して大幅に改良されたバージョンを得る)、 B. LLMが提供する証明を用いて、定義、命題、補題、定理といった簡素な数学テキストに簡潔に絞りました。 C. アリストテレスのシステムを一晩中(API経由で)実行しました。今朝、Leanで約700行の完全形式化されたバージョンを受け取りました。 コードはコンパイルされるため、LLMで生成された証明が正しい解に導いたことを証明する証明書が手に入りました。さらに、自分の力任せよりも優れた概念的証明を得た。さらに、こうした代数問題のより広いクラスに広げていくつもりです。 小さなプロジェクトですが、私にとっては大きな節目です。今では、オーケストレーションを組み合わせて数学定理の発見、形式化、証明を真に助けるツールを手に入れました。これは簡単なことではありません。 問： 1. 将来的にどのように拡大していくのか? 2. そのような任務で成功するにはどれほどの訓練が必要か?...