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が必要です。
永続的なLean言語サーバーにより、一度ウォームアップすればコンパイルチェックが約30秒から約0.4秒に短縮されます。
HNでの議論
29- muds
興味深い仕事だ。これはAUTOLEANプロジェクト（https://github.com/T3S1AMAX/autolean）のラッパーなのか？
- homarp
数学形式化エンジンを内蔵したターミナルAIコーディングアシスタント。平易な言葉で問題を説明すると、それをLean 4の定理に変換し、形式証明を試みる。
- eisbaw
難しいのは、あなたの不正確な平易な英語の記述を、正しくLeanとして捉えて形式化することだ。