MathCode、数学的コーディングエージェント

概要 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 mathcode setup.sh はリリースチェックアウトを準備し、バンドルされたランタイムとLeanツールチェーンをダウンロードし、ユーザーローカルのmathcodeランチャーをインストールします。 以下で試してみてください: mathcode -p "prove that the square of an even number is even" 出力はLeanFormalizations/に書き込まれます。ブラウザUIは ./run webui 経由で利用可能です。 機能 永続的なLean REPL 永続的なLean言語サーバーは、一度のウォームアップ後、約30秒ではなく約0.4秒でコンパイルチェックをもたらします。 定理ライブラリ 証明された各定理は自動命名、保存され、インポート可能になるため、プロバーとプランナーはそれを再利用できます。 公理ライブラリ 会話上の仮定を、永続的でコンパイルチェック済みの、一貫性がレビューされたLean宣言として保存します。 Lean LSP統合 leansearch.net と Loogle を検索して検証済みのMathlibの補題を見つけ、構造化されたLSP診断を使用して修正を行います。 Obsidian定理グラフ 定理から補題への依存関係を知識グラフとして視覚化するObsidianボールトを生成します。 エージェントモード証明 各証明はインタラクティブなセッションとなり、エージェントは候補を作成し、エラーを読み、再コンパイルします。 サブゴールのツリー 複雑な定理を独立したサブゴールに分解し、並列に証明してから、それらを再結合します。 マルチプランナー 多様な証明戦略のために複数のプランナーを並列実行し、プロバーが最良のアプローチを選択します。 引用 研究で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} } BibTeXをコピー 数学形式化と証明のパイプラインはAUTOLEANプロジェクトに基づいています。