>>749 余談
>13.8　フェルマーの最終定理と証明支援系

ここは、池上氏の記事のあと 下記進展があった
が、思うに 「グロタンディーク宇宙とSGA」のような
グロタンディークの代数幾何の定理を 存分に取り入れていると思われる

もし、下記のAnthropicの発表の詳細にアクセスできる人がいれば
見て 教えてちょ

(参考)
https://finance.biggo.jp/news/66299417-e5ad-479a-a0d3-ff876c8251e3
finance.biggo.jp
Claude、11日間でフェルマーの最終定理を形式化検証、清華大学姚班出身者が主導
2026-09-05

Anthropicは9月4日、AIモデル「Claude」がほぼ自律的に11日間稼働し、フェルマーの最終定理について初のエンドツーエンドのコンピュータ検証可能な証明を完成させたと発表した。Claudeは約1300万行のLeanコードを生成し、約3万300個の定理を構築、うち2万9500個が最終証明に組み込まれた。規模は世界最大の数学定理ライブラリ「Mathlib」の5倍超、総消費量は約60億出力トークンに達した。プロジェクトは清華大学姚班出身でコロンビア大学助教授の彭天翼氏が主導し、同氏のチームが開発した「Prove2Me」プラットフォームがマルチエージェント協調の混乱を解消。当初数年かかると見込まれた形式化工程を2週間未満に圧縮した。この成果は数学の検証方式が人手による査読からコンピュータ自動検証へ移行するパラダイムシフトを示すものだ。