Harmonicは2026年3月、世界初の形式数学AIエージェント「Aristotle」を無料公開した。英語で問題を入力するだけで、Lean 4による機械検証済みの数学的証明を自律的に生成・検証する。r/singularityでは206↑・21コメントを集め、「AlphaProofが非公開のままである中、Harmonicが無料で公開したのは画期的」と評価を受けている。
Harmonic「Aristotle」とは｜世界初の形式数学AIエージェント
AristotleはHarmonicが開発した完全自律型の数学AIエージェントで、証明補助言語「Lean 4」を用いて数学的定理を形式的に証明する。公式サイトによればProofBench（Vals AI）のランキングで1位を獲得しており、2位との差は15%以上。2025年の国際数学オリンピック（IMO）問題でも金メダル相当の成績を記録している。
注目を集めるきっかけとなったのは、Erdős問題#1026（Erdős問題#124の亜種）をAristotleが数時間以内に自律解決・Lean形式化したという報告だ。テレンス・タオも言及したこの問題に対し、Aristotleは人間の介入なしに証明を完成させた。Harmonicはシリーズ Cで1.2億ドルを調達済みで、同社の数学推論研究の集大成がこのエージェントにあたる。
技術的特徴と対応範囲
Aristotle Agentの主な機能
| 機能 | 詳細 |
|---|---|
| 自律稼働時間 | 最長24時間、人間の介入なしで証明を継続 |
| 入力形式 | 英語の自然言語で問題を記述するだけでOK |
| 出力形式 | Lean 4の機械検証済みコード（ライブラリ対応済み） |
| ファイル編集 | Leanプロジェクト・コードリポジトリを直接編集 |
| ベンチマーク | ProofBench 1位（2位比+15%）、IMO 2025金相当 |
最大の技術的優位は「形式検証」にある。LLMが自然言語で生成した証明は人間が確認しなければ正誤が不明だが、Lean 4の型チェッカーを通過した証明は原理的に正しいことが保証される。これを24時間自律で行えるのがAristotleの核心だ。
また、出力コードはMathlib等の主要形式化プロジェクトにそのまま取り込める「ライブラリ対応済みコード」として生成される。単なるプロトタイプでなく、数学コミュニティの実際のワークフローに直結する設計になっている点が評価されている。
Leanstralとの違い
同じLean 4対応のAIとして比較されるのがMistral AIの「Leanstral」だ。LeanstralはオープンソースのLean 4コードエージェントで、複数パスによる精度向上を特徴とする。しかし性質が異なる。
Leanstralは「Lean 4を書くためのコーディングアシスタント」に近い位置付けで、Aristotleは「数学の難問を自律で解くエージェント」として設計されている。両者は競合というよりも補完的な関係にあると言えるだろう。
Redditの反応（206↑）
r/singularityのスレッドは206↑・21コメントを記録。注目コメントを紹介する。
51↑ — u/[top commenter]
"形式検証こそが他の『AIが数学をやった』系発表と本質的に違う部分。LLMが自然言語で生成した証明はそれが正しいかわからないが、型チェックを通過したLean証明は構造的に正しい。DeepMindがAlphaProofを非公開のままにしている中、これを無料公開しているのはかなり本気だと思う"
9↑ — u/[commenter]
"Harmonicはトップ企業で、この研究はブレークスルーにつながり得る"
1↑ — u/[commenter]（懐疑派）
"自分には使いこなせないが、本当に使える人たちが長く無料で使い続けられることを願う。『今は無料』はいずれ変わる"
Aitly編集部の見解
編集部まとめ
Aristotleが示したのは「AIが数学を解く」から「AIが数学的に正しい証明を自律生成できる」への質的転換だ。自然言語の証明には常に誤りのリスクが伴うが、Lean 4の型システムで検証済みの出力はそのリスクを根絶する。これは数学そのものの信頼性インフラが変わることを意味する。
現時点での制約として、Erdős問題#124の「弱化版」を解いたという点は注意が必要だ。オリジナルの問題ではなく、既知の結果に帰着できる亜種であったことをテレンス・タオ自身が指摘している。しかしその上でも、AIが形式的証明を自律生成し数学コミュニティのライブラリに直接貢献できる段階に達したことは評価に値する。
競合のDeepMind AlphaProofが非公開である中、Harmonicが研究グラント100万ドルの提供と合わせて無料公開に踏み切った戦略は、数学AI分野のデファクトスタンダード獲得を狙ったものと読める。今後、Mathlibへの貢献量や未解決問題への適用事例が同社の評価軸になるだろう。
AIツールとして見るならば、Aristotleは現状「数学研究者・形式検証エンジニア向け」の専門ツールだ。英語で問題を入力するだけという入口のシンプルさに対し、出力を活用するにはLean 4の知識が前提となる。一般ユーザーへの波及は、Lean教育ツールや自動化パイプラインとの統合が進んだ次のフェーズを待つ必要があるだろう。
