MathCode、数学問題から Lean 4 定理証明を自動生成するターミナル AI コーディングアシスタントとして公開
本文の状態
日本語全文を表示中
詳細モードで約3分の本文を読めます。
同じ出来事の情報源
この情報源を基点に整理
TLDR AI
MathCode は、自然言語の数学問題を Lean 4 の定理に変換し自動証明を試みるターミナル型 AI コーディングアシスタントであり、永続的な REPL や知識グラフ機能を備えている。
AI深層分析を開く2026年8月18日 22:02
AI深層分析
キーポイント
Lean 4 自動変換と証明機能
MathCode は自然言語で記述された数学問題を自動的に Lean 4 の定理に変換し、Persistent Lean REPL を用いて証明を試みる。
高度な証明戦略と統合機能
Tree-of-Subgoals や Multi-Planner による並列処理に加え、Obsidian との連携で定理間の依存関係を可視化する知識グラフを生成する。
開発環境と実用性
macOS (arm64) または Linux (x86_64) 上で動作し、codex CLI をバックエンドとして利用可能なオープンソースツールとして提供される。
MathCode の基本情報
MathCode は Team Math-AI が開発した先端的な数学コーディングエージェントであり、2026年4月に公開された。
証明パイプラインの基盤
数式の形式化と証明のパイプラインは、AUTOLEAN プロジェクトをベースに構築されている。
重要な引用
MathCode is a terminal AI coding assistant with a built-in math formalization engine.
Give it a math problem in plain language and it will automatically convert it into a Lean 4 theorem and attempt a formal proof
A persistent Lean language server brings compile checks to ~0.4s after a one-time warmup, instead of ~30s.
"The math formalization and proving pipeline is based on the AUTOLEAN project."
編集コメントを表示
編集コメント
MathCode は、AI を用いた数学的証明の自動化において実用的な進歩を示す。特にコンパイル速度の劇的な改善と、知識グラフとの連携は、研究現場での活用可能性を高める要素である。
Source Article
元記事を日本語で読む
本文に関係しない購読案内、埋め込み通知、サイト内プロモーションは除いています。
概要
MathCode は、組み込みの数学形式化エンジンを持つターミナル型 AI コーディングアシスタントです。自然言語で記述された数学の問題を入力するだけで、自動的に Lean 4 の定理に変換し、永続的な Lean REPL や再利用可能な定理・公理ライブラリ、エージェントによる証明機能、そして Obsidian 連携の知識グラフを活用しながら、形式証明への挑戦を試みます。
クイックスタート
動作には、macOS（arm64）または Linux（x86_64）が必要で、デフォルトのバックエンドとして codex CLI を用意する必要があります。
git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login
mathcodesetup.sh スクリプトは、リリースのチェックアウトを準備し、バンドルされたランタイムと Lean ツールチェーンをダウンロードして、ユーザーローカルの mathcode ランチャーをインストールします。以下のように試してみてください:
mathcode -p "prove that the square of an even number is even"出力先は LeanFormalizations/ フォルダになります。ブラウザ用 UI は ./run webui コマンドで利用可能です。
特徴
永続的な Lean REPL
一度ウォームアップするだけで、コンパイルチェックが約 30 秒から約 0.4 秒に短縮される、永続的な Lean ラングサーバーを提供します。
定理ライブラリ
証明されたすべての定理は自動的に命名され保存されるため、証明エンジンとプランナーが再利用できます。
公理ライブラリ
会話形式の仮定を、永続的でコンパイルチェック済み、かつ整合性が確認された Lean 宣言として保存します。
Lean LSP の統合
検証済みの Mathlib 補題を検索するために leansearch.net と Loogle を利用し、構造化された LSP ダイアグノスティクス（診断情報）を用いて修正を行います。
Obsidian 定理グラフ
定理と補題の依存関係を知識グラフとして可視化する Obsidian バルトを生成します。
エージェントモードによる証明
各証明は、エージェントが候補を記述し、エラーを読み込み、再コンパイルを行うインタラクティブなセッションとなります。
サブゴールツリー (Tree-of-Subgoals)
複雑な定理を独立したサブゴールに分解し、並列で証明した後、それらを結合します。
マルチプランナー (Multi-Planner)
多様な証明戦略のために複数のプランナーを並列実行し、プロバーが最適なアプローチを選択します。
引用
研究で MathCode を使用する場合は、以下を引用してください：
@misc{mathcode2026,
title = {MathCode: A Frontier Mathematical Coding Agent},
author = {Team Math-AI},
journal = {math-ai-org.github.io},
year = {2026},
month = {April},
url = {https://github.com/math-ai-org/mathcode}
}数式の形式化と証明パイプラインは、AUTOLEAN プロジェクトに基づいています。
原文を表示
Overview
MathCode is a terminal AI coding assistant with a built-in math formalization engine. Give it a math problem in plain language and it will automatically convert it into a Lean 4 theorem and attempt a formal proof — with a persistent Lean REPL, reusable theorem and axiom libraries, agentic proving, and an Obsidian knowledge graph.
Quick Start
Requires macOS (arm64) or Linux (x86_64), plus the codex CLI for the default backend.
git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login
mathcodesetup.sh prepares the release checkout, downloads the bundled runtime and Lean toolchain, and installs a user-local mathcode launcher. Try it with:
mathcode -p "prove that the square of an even number is even"Outputs are written to LeanFormalizations/. A browser UI is available via ./run webui.
Features
Persistent Lean REPL
A persistent Lean language server brings compile checks to ~0.4s after a one-time warmup, instead of ~30s.
Theorem Library
Every proved theorem is auto-named, stored, and made importable so the prover and planner can reuse it.
Axiom Library
Store conversational assumptions as persistent, compile-checked, consistency-reviewed Lean declarations.
Lean LSP Integration
Searches leansearch.net and Loogle for verified Mathlib lemmas and uses structured LSP diagnostics for repairs.
Obsidian Theorem Graph
Generates an Obsidian vault that visualizes theorem-to-lemma dependencies as a knowledge graph.
Agent-Mode Proving
Each proof becomes an interactive session where the agent writes candidates, reads errors, and recompiles.
Tree-of-Subgoals
Decomposes complex theorems into independent subgoals and proves them in parallel, then stitches them back.
Multi-Planner
Runs multiple planners in parallel for diverse proof strategies; the prover picks the best approach.
Citation
If you use MathCode in research, please cite:
@misc{mathcode2026,
title = {MathCode: A Frontier Mathematical Coding Agent},
author = {Team Math-AI},
journal = {math-ai-org.github.io},
year = {2026},
month = {April},
url = {https://github.com/math-ai-org/mathcode}
}The math formalization and proving pipeline is based on the AUTOLEAN project.
関連記事
今日のまとめ
AIデイリーブリーフで今日の重要ニュースをまとめ読み