MathCode：一个具备Lean 4形式化的数学编码智能体

MathCodeは、ターミナルベースのAIコーディングアシスタントで、Lean 4を使用して数学の問題を形式化し、証明します。自分でLeanコードを書く代わりに、平易な英語で問題を与えると、定理を生成し、証明を試みます。永続的なREPLと再利用可能な定理のライブラリを備えています。

主な機能

• 永続的なLean REPL： 一度ウォームアップすれば、コンパイルチェックが約30秒から約0.4秒に短縮されます。
• 定理ライブラリ： 証明された定理はすべて自動的に名前が付けられ、保存され、再利用のためにインポートできます。
• 公理ライブラリ： 会話上の仮定を永続的な、コンパイルチェック済みのLean宣言として保存します。
• Lean LSP統合： leansearch.netとLoogleで検証済みのMathlib補題を検索し、構造化されたLSP診断を使用して修復します。
• Obsidianの定理グラフ： 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 -p "prove that the square of an even number is even"

出力はLeanFormalizations/に書き込まれます。ブラウザUIは./run webuiで利用できます。

このツールは、形式検証やAI支援の定理証明に取り組む数学者、研究者、開発者を対象としています。