数学の証明を自動化するターミナル型のAIコーディングエージェント。自然言語で書いた数学の問題をLean 4（定理証明支援系プログラミング言語）の定理に自動変換し、形式証明を試みる。Lean 4はコードのように命題や証明を記述し、コンパイラが論理の正しさを機械的に検証できるツールで、Mathlibという10万件を超える定理・補題のライブラリが整備されている。2026年8月にはv0.3.0がリリースされ、ローカルWebUIのワークフローが完成したほか、論文をそのままvaultに取り込む機能やエージェント型のLeanツール群が拡張された。
主な特徴
- 自然言語からLean 4定理への自動変換:
mathcode -p "prove that the square of an even number is even"のようにコマンドで問題を渡すと、Lean 4の定理として形式化し証明を試みる。出力はLeanFormalizations/ディレクトリに保存される - 常駐Lean REPLによる高速コンパイルチェック: 起動時に一度だけMathlibを読み込むウォームアップを済ませることで、以降のコンパイルチェックを約30秒から約0.4秒まで短縮する。LeanGoal（目標検査）・LeanCheck（コンパイルとフィードバック）・LeanVerify（最終的な厳密検証）といった専用ツールを組み合わせて使う
- Mathlib検索とサブゴール分解: leansearch.netやLoogleと連携してMathlibの既存補題を検索し、複雑な定理はサブゴールに分解して並列に証明を試みる。複数のプランナーが異なる証明戦略を競わせ、最良の結果を選ぶ
- 定理・公理ライブラリの蓄積:
/theorem-storeで証明済みの定理を、/axiomatizeで会話中に出た仮定を永続的なライブラリとして保存し、以降の証明で再利用できる - Obsidianナレッジグラフによる可視化: 証明した定理間の依存関係をObsidianの知識グラフとして自動生成し、規模の大きい形式化プロジェクトでも全体像を把握しやすくする
- ローカルWebUIとマルチLLM対応: v0.3.0でローカルWebUIのワークフローが完成し、
./run webuiから利用できる。バックエンドはデフォルトのOpenAI Codex CLIに加え、ANTHROPIC_API_KEYを設定したAnthropic系モデル、Amazon Bedrock・Google Vertex AI・Azure AI Foundry・OpenRouter経由のモデルにも対応する
料金
MathCode自体はオープンソース(Apache 2.0)としてGitHub上で公開されており、クローンしてセットアップスクリプトを実行すれば利用できる。ただし証明の生成にはLLMを呼び出すため、別途モデル提供元側の利用料がかかる。デフォルトはOpenAIのCodex CLI経由の認証（codex auth login）で、環境変数を切り替えればAnthropicのAPIキーや、Bedrock・Vertex AI・Azure AI Foundry・OpenRouterといった他のプロバイダー経由のモデルも利用できる。
料金は2026年8月時点の情報です。MathCode自体に価格プランは設けられていませんが、利用するLLMプロバイダー側の料金は変更される可能性があるため、詳細は公式サイトや各プロバイダーの案内をご確認ください。
メリット・デメリット
✅ メリット
- 自然言語で書いた数学の主張をLean 4定理への変換から形式証明までワンストップで行える
- 常駐Lean REPLにより、証明の試行錯誤で発生しがちなコンパイル待ち時間を大幅に短縮できる
- 証明済みの定理・公理をライブラリとして蓄積し、以降の証明で再利用できる
- leansearch.netやLoogleとの連携でMathlibの既存補題を探せる
- OpenAI・Anthropic・Bedrock・Vertex AI・OpenRouterなど複数のLLMプロバイダーから選べる
⚠️ デメリット
- Lean 4という特定の証明支援系に用途が限定され、Coq・Isabelleなど他の証明支援系では使えない
- 対応OSはmacOS（arm64）とLinux（x86_64、AVX2対応CPU）のみで、Windowsをネイティブにサポートしない
- MathCode自体に料金プランはないが、LLM側の利用料は別途必要になる
- Lean 4やMathlibについての前提知識がないと、証明が失敗した際の原因特定や対処が難しい場面がありうる
類似サービスとの比較
| 比較項目 | MathCode | Lean Copilot | Harmonic Aristotle |
|---|---|---|---|
| 提供元 | Math-AI | LeanDojoチーム（学術プロジェクト） | Harmonic |
| 形態 | ターミナル型AIコーディングエージェント（OSS） | Lean証明中に使うタクティク支援ツール（OSS） | Web・モバイル・APIで提供される商用プロダクト |
| 主な用途 | 自然言語の問題をLean 4定理へ変換し証明まで自動化 | 証明中のタクティク提案・補題検索・証明探索の支援 | IMOレベルの高難度な証明や研究・企業向けの形式検証 |
| モデルの扱い | Codex CLI／Anthropic等、複数プロバイダーを切り替え | 事前学習済みモデルまたは持ち込みモデルをローカル/クラウドで実行 | Harmonic独自の専用モデルを利用 |
| 料金 | 無償公開（LLM利用料は別途） | 無償公開 | 商用（詳細は要問い合わせ） |
このほか、Lean 4の証明データセットや検索基盤を提供する研究プロジェクトのLeanDojo、Claude CodeやCodex CLIのような汎用AIコーディングエージェントも、広い意味では比較対象になりうる。ただし後者はLean 4の形式証明に特化した機能（常駐REPL・定理ライブラリ・Mathlib検索連携など）を持たない点がMathCodeとの違いになる。
こんな人におすすめ
- Lean 4で数学の定理や命題を日常的に形式化・証明している研究者や学生
- 自然言語で書いた命題をすばやくLean 4の定理として書き起こしたい人
- Codex CLIなど既存のAIコーディングエージェントの延長で、Lean証明作業も自動化したい人
- 証明の依存関係を可視化しながら、規模の大きい形式化プロジェクトを管理したい人
まとめ
MathCodeは、自然言語で書いた数学的主張をLean 4の形式証明へと変換するターミナル型のAIエージェントである。常駐Lean REPLによる高速なコンパイルチェック、Mathlib検索との連携、証明済み定理のライブラリ化など、実際にLean 4で形式化作業を進める際の摩擦を減らす工夫が随所に盛り込まれている。一方でLean 4という特定の証明支援系に用途が限定され、対応OSもmacOSとLinuxに絞られるため、対象となる読者はLean 4での証明を日常的に書く層に絞られる。2026年8月時点でv0.3.0がリリースされ、WebUIの追加など機能拡張が続いている。