要点：
陶哲轩は AI ツールを利用して多項式 Freiman-Ruzsa 予想の証明を形式化し、数学研究における人工知能の広範な応用を象徴し、数学界に衝撃を与えました。
彼は数学研究者が AI ツールを正しく使用することを強調し、形式化された証明の主流化によって、人間が読めるだけでなく機械でも解ける証明が生まれ、数学がプログラミングの一形態になる可能性があると考えています。
陶哲轩のチームは Blueprint ツールを使用して、証明プロセスを処理しやすい部分に分解し、多くの貢献者が並行して作業することで、PFR 予想を形式化することに成功しました。
中国のウェブサイト「站长之家（ChinaZ.com）」の 12 月 6 日のニュースによると、陶哲轩は最近、AI ツールを利用して多項式 Freiman-Ruzsa 予想の証明を形式化し、この成果は数学界の広範な関心を引きました。彼はブログで、Lean4 で Blueprint を使用して証明を形式化するプロセスを詳細に記録しています。このプロジェクトは 3 週間かかり、多項式 Freiman-Ruzsa 予想の証明を形式化することに成功し、数学研究における人工知能の力に驚嘆しました。
陶哲轩はこの成果の解釈で AI ツールの正しい使用の重要性を強調しています。彼は形式化された証明の主流化によって、人間が読めるだけでなく機械でも解ける証明が生まれ、数学がより効率的なプログラミングの形態になる可能性があると考えています。彼は特に Blueprint ツールを推奨し、チームが Lean に関連する人間が読める証明の「ブループリント」を作成できるようにしました。このプロジェクトでは、緑色のバブルや四角形は完全に形式化された補題や定義を示し、青色は形式化の準備ができた補題や定義を示しており、プロジェクトの形式化の進捗の概要を示しています。
彼は Blueprint を使用してプロジェクトを処理しやすい部分に分解する効果を強調し、大量の並行作業を可能にしました。これにより、Lean プログラミングスキルを持たない数学者でも形式化プロジェクトをリードすることができます。陶哲轩のチームの目標は、「pfr」バブルにつながるすべてのバブルを緑色にすることであり、最終的に Lean で PFR 予想を成功裏に証明し、プロジェクトの主要な目標を達成しました。
彼の成果は、数学研究の将来についての議論を引き起こしました。一部の人々は、形式化が主流の数学で重要なトレンドになると考えており、ほとんどの証明は類似のシステムでのみ完了し、人間が読める論文を書く必要がなくなると予想しています。しかし、陶哲轩は「コンピュータ支援証明」と「理解できない / 偶然の証明を提供できない」とを混同しないように警告し、形式化が理解する証明の重要性を弱めるものではないと強調しています。この成果は形式化が主流の数学で注目されていることを示し、将来の数学研究の可能な方向を示しています。