スウォームコーディングの未来を垣間見た。エージェントの群れは、私たちがソフトウェアを構築する方法を根本的に変えるだろう。

Axiom は、有限単純群の分類の完全な Lean 自動形式化を発表した。これは何世代にもわたる 100 人以上の数学者によって築かれた約 15,000 ページの証明で、現在は約 5,000 万行の Lean に変換され、24 日で検証された。エージェントの群れは GitHub を通じてタスクを分担し、証明を書き、互いにレビューし、成果を統合する過程で、公表された証明中の数百件の重大な誤りを修正した。これは、数学史上最大の証明が完全に計算機で検証可能になったことであり、エージェントの群れが孤立した定理だけでなく、相互に関連した数学全体を担えることの具体的な実証であるため重要である。

• Elvis Saravia2026-10-27 14:51
• Kim2026-10-27 14:45