2026-10-31 05:39:57
AI、24日で4,000万行に及ぶCFSGの形式的証明を完成させた
Guru Clubによると、10月31日、AxiomのマルチエージェントAIシステムが、有限単純群の分類(CFSG)に関する人類史上最大規模の数学的証明の形式検証を完了した。世界中の100人を超える著名な数学者が執筆し、完成までに1世紀以上を要した全15,000ページに及ぶこの証明の検証作業を、AIシステムはわずか24日で完了した。この取り組みにより、4,000万行を超えるLeanコードライブラリが作成され、現在ではコード行数で最大のオープンソースソフトウェアプロジェクトとなり、Linux kernel、Chromium、Firefox、LLVM、GCC、FFmpegを上回っている。また、AIシステムは人間が作成した元の証明に欠落箇所があることを特定し、その修正を完了するための新たな数学的定理も提示した。