MathCode：数学の問題をLean 4の定理に変換し、自動証明するAIコーディングエージェント

MathCode, Mathematical Coding Agent

MathCodeは、ターミナル上で動作するAIコーディングアシスタントで、数学の形式化エンジンを内蔵しています。自然言語で数学の問題を与えると、自動的にLean 4の定理に変換し、証明を試みます。特徴として、永続的なLean REPL（コンパイルチェックが約0.4秒）、再利用可能な定理ライブラリ、公理ライブラリ、Lean LSP統合、Obsidianによる定理グラフの可視化、エージェントモードでの証明、サブゴールの並列証明、複数のプランナーによる戦略探索などがあります。macOS (arm64) または Linux (x86_64) で動作し、`codex` CLIが必要です。