math-ai-org/mathcode

MathCode – AI駆動のLeanコード補助ツール

何であるか – MathCodeは、Lean定理証明言語で形式的証明を書く、検証する、確認するのを支援するターミナルベースのAIコードエージェントです。Leanツールチェイン、軽量なWeb UI、およびモデルがLeanと対話できる「スキル」のセットをバンドルしています（宣言の検索、候補の検証、証明の確認など）。

主な機能

• 目標指向の証明作成 – 自然言語で目標（例：「偶数の平方は偶数であることを証明する」）を提示すると、エージェントはLeanコードを反復的に生成し、Leanツールを呼び出し、証明を改善します。
• Leanバックエンド – インプロセスのLean REPL、ピン止めされたサブプロセス、または外部のKimina Leanサーバーを使用してコンパイルおよび検証が可能です。
• 永続的ライブラリ – 証明済みの定理（/theorem-store）や会話形式の公理（/axiomatize）をバージョン管理可能なボルトに保存でき、後で再利用できます。
• Obsidianグラフエクスポート – 定理の依存関係を可視化した知識グラフを生成し、Obsidianで開くことができます。
• Web UI – 軽量なブラウザインターフェース（./run webui）で、ローカルデーモンを起動し、ターミナルと同一のインタラクティブセッションを表示します。
• スケジューリング – /loop 10m … のようなスラッシュコマンドで、リマインダーまたは定期的なチェック用の繰り返しプロンプトを設定できます。

インストールと設定

1. リポジトリをクローンし、bash setup.sh を実行します。スクリプトは以下の作業を行います：
   • 必要に応じて事前にビルドされたランタイムバンドル（mathcode-vX.Y.Z-<os>-<arch>.tar.gz）をダウンロードします。
   • SHA-256チェックサムでダウンロードを検証します。
   • ユーザー専用のランチャ（~/.local/bin/mathcode）をインストールします。
   • バンドルされたLeanツールチェイン（.local/elan）とキャッシュされたMathlibスナップショットをセットアップします。
2. Linuxでは bubblewrap（bwrap）と socat が必要です。macOSではバンドルは即座に動作します。
3. デフォルトのOpenAIバックエンドモデルを使用したい場合は、codex CLIをオプションでインストールできます。

通常のワークフロー

# インタラクティブセッションを開始
mathcode -p "prove that the square of an even number is even"
# または入力をパイプで渡す
echo "hello" | mathcode -p

# Web UIを起動
./run webui

セッション内ではスラッシュコマンドを使用できます：

• /goal <budget> <objective> – トークン予算を設定し、エージェントに証明作業を依頼します。
• /theorem-store …, /axiomatize … – 永続的定理／公理ライブラリを管理します。
• /obsidian generate – Obsidianグラフを更新します。
• /loop … – 繰り返しプロンプトをスケジュールします。

設定オプション（環境変数）でシステムをカスタマイズできます。たとえば：

• MATHCODE_GOAL_MAX_TOKEN_BUDGET – 目標に対するトークン予算の上限を設定します。
• MATHCODE_MAX_CHAINED_COMMAND_INPUTS – エージェントが実行できるネストされたツール呼び出しの数を制限します。
• MATHCODE_LEAN_REPL – インプロセスREPLを使用するように強制します。
• MATHCODE_KIMINA_SERVER および関連する変数 – 外部のKimina Leanサーバーへの接続先を指定します。

メンテナンス

• bash setup.sh --status は、バイナリ、チェックサム、バンドルされた ripgrep の健全性を確認します。
• bash setup.sh --clean はインストールアーティファクトを削除しますが、証明ボルトやLean形式化は保持します。

対象ユーザー – Leanで作業し、AI駆動のアシスタントで定理証明を高速化し、Mathlibを探索し、再利用可能な形式的結果のライブラリを維持したい研究者、学生、開発者です。

---

上記のすべての詳細はリポジトリのREADMEから直接引用されています。追加の機能は推測されていません。