math-ai-org/mathcode

MathCode – 形式数学のためのコーディングアシスタント

概要

• MathCodeは、Lean 4証明支援系と密接に統合された、ターミナルおよびブラウザベースのコーディングアシスタントです。コードや形式的な証明の記述、現在の証明ゴールのクエリ、Leanライブラリの検索、および証明の正当性検証を行うことができます。

主な機能

• Lean 4による証明チェック – MathCodeは、ゴールを検査し、宣言を検索し、候補となる補題をテストし、Leanの厳密な検証器を実行して証明を確定させることができます。
• デュアルUI – コマンドラインインターフェース (mathcode …) を使用するか、数学や図をレンダリングするローカルWebUIを起動できます。
• ナレッジボルト – 検証済みの定理とその明示的な仮定はObsidianボルトに保存・探索でき、個人の結果ライブラリや依存関係グラフを構築できます。
• 拡張可能なスキル – Python分析ツール、カスタム“MCP”プラグイン、その他プロジェクト固有のスキルをエージェントに追加できます。

はじめ方

1. リポジトリをクローンし、提供されている setup.sh スクリプトを実行します。
2. 必要な codex バックエンドを認証します (codex auth login)。
3. ターミナルセッションには ./run を、ブラウザUIには ./run webui を実行します。
4. 完全な証明支援機能が必要な場合は、bash setup.sh --with-lean を使用してLean 4 (約10 GiB) をインストールしてください。

対応プラットフォーム

• macOS Apple Silicon (arm64)
• Linux x86_64 (glibcおよびAVX2が必要)

典型的なワークフロー

mathcode -p "prove that the square of an even number is even"

このコマンドは対話型セッションを開始し、MathCodeが補題を提案し、Leanでチェックを行い、最終的な定理をボルトに記録します。

ドキュメントとコミュニティ

• オンラインドキュメント: https://math-ai-org.github.io/mathcode/docs/
• リリース、イシュートラッカー、DiscordコミュニティへのリンクはREADMEに記載されています。

重要性 MathCodeは、日常的なコーディング環境と形式数学の間のギャップを埋めます。Leanの検証を使い慣れたターミナル/WebUIワークフローに組み込むことで、開発者や研究者が普段のツールを離れることなく、機械検証された証明を簡単に作成できるようになります。

引用 研究でMathCodeを使用する場合は、以下のように引用してください:

@misc{mathcode2026,
  title = {MathCode: A Frontier Mathematical Coding Agent},
  author = {Team Math-AI},
  year = {2026},
  url = "https://github.com/math-ai-org/mathcode"
}