MathCodeは、自然言語で書かれた問題をLean 4の定理に変換し、形式的な証明を試みます。

Why it matters

MathCode shows how AI math tools are shifting from one-off answers toward persistent, reusable proof libraries, with Lean's compiler providing a hard verification layer.

公開されている資料は、Yifan Zhang (@yifanzhang_) を Math-AI と最もはっきり結びつけており、Math-AI は MathCode の背後にあるオープン研究コミュニティです。MathCode は、日常の言葉で書かれた数学を Lean 4 の命題に変換し、形式的な証明を試み、成功した結果を後で再利用できるよう保存するターミナル型の AI コーディングアシスタントです。

MathCodeのプロジェクトページ はプロジェクトを 2026 年 4 月に日付付けしています。MathCode は新規ローンチというより、継続的なオープンソース研究プロジェクトとして読むべきです。

その区別は重要です。なぜなら MathCode の最も強力なアイデアは初期リリースを超えているからです：Zhang のグループは形式数学を、エージェントが徐々に拡張し、検索し、再利用できるコードベースとして扱っています。各成功した定理は次の証明のためのインフラストラクチャになり得ます。

Zhang は自らを Princeton University の博士課程の学生であり、Princeton AI Lab Fellow として、言語モデルの推論、強化学習、事前学習、モデルアーキテクチャに取り組んでいると記述しています。彼の公開研究ポートフォリオには数学テキストのキュレーションや推論システムが含まれており、これが MathCode が非構造化の数学的言語を耐久性のある機械可読オブジェクトに変えることに重点を置く理由を説明する助けになっています。

Math-AI は自らをオープン研究コミュニティとして提示しており、コード、モデル、研究資料は GitHub と Hugging Face を通じて公開されています。公開資料は MathCode を商用サービスとして提示しておらず、プロジェクトに公開された価格、収益、顧客数の数字はありません。

コーディングエージェントのように構築された証明アシスタント

オープンソースの MathCode リポジトリ はワークフローを macOS の Arm プロセッサー向けと x86_64 システムの Linux 向けのターミナルアプリケーションとしてパッケージ化しています。ユーザーは例えば「偶数の二乗は偶数であることを証明せよ。」のようなプロンプトを送信できます。MathCode はその要求を Lean の定理として形式化し、証明候補を生成し、それらをコンパイルし、Lean のエラーを利用して別の試行を誘導します。

ローカルセットアップは意図的な製品選択です。MathCode はバンドルされた Lean ツールチェーンをインストールし、永続的な言語サーバーを維持し、生成された作業を LeanFormalizations ディレクトリに書き込みます。ブラウザインターフェースも含まれますが、ターミナルが主要なワークフローであり続けます。

デフォルトの経路は OpenAI の Codex CLI とその認証システムに依存します。リポジトリは Anthropic-compatible および OpenAI-compatible なバックエンドも文書化しています。その柔軟性により研究者は基盤となるモデルをある程度制御できますが、MathCode の証明品質、レイテンシ、および運用コストは選択する外部モデルプロバイダーに部分的に依存します。

MathCodeのドキュメント によれば、永続的な Lean プロセスはウォームアップ後のコンパイルチェックを概ね 0.4 秒に短縮し、Lean を繰り返し起動してライブラリを読み込まなければならない場合のおよそ 30 秒と比べて高速化されるとしています。これらの数値はプロジェクト側のもので、独立したベンチマークではありません。それでも設計は具体的なエージェント問題に対処しています：フィードバックサイクルが長いと反復的な証明修正が高コストになりがちですが、永続コンパイラはモデルが失敗して再試行することを迅速に可能にします。

エージェントは定理をサブゴールに分割し、いくつかの計画戦略を並列で実行し、成功した断片をつなぎ合わせて最終的な証明を作ることができます。既存の Mathlib 補題を探すために LeanSearch と Loogle を検索し、構造化されたコンパイラ診断を証明ループにフィードバックすることも行います。

MathCode は基盤となる形式化と証明パイプラインを提供する AUTOLEANプロジェクト を基に構築されています。Math-AI の貢献は周辺の作業環境です：永続状態、ライブラリ検索、反復修復、並列計画、およびエージェントが既に証明したものを保持するためのインターフェースです。

Zhangは使い捨ての回答ではなく記憶を重視している

最も重要な機能は、MathCode の過去の作業の扱いです。正常にコンパイルされた定理は自動的に名前が付けられ、再利用可能な Lean ライブラリに書き込まれ、後のセッションにインポートできます。ユーザーは会話上の前提をコンパイルでチェックされた公理宣言として保存することもできます。

それは有用性と同時にリスクも生みます。Lean は証明が記載された前提から導かれることを検証できますが、ユーザーの前提が世界を正確に記述していることを保証することはできません。MathCode は保存された公理の一貫性レビュー用ツールをドキュメントで含むとしていますが、結果として得られる知識ベースの信頼性は依然として慎重な仕様作成とライブラリ管理に依存します。

MathCode はまた定理や補題の依存関係をマップする Obsidian vault を生成します。そのグラフは Zhang のより広い研究方向性の実用的な表現です：数学的出力はチャットセッションが終わったときに消えるのではなく、ナビゲート可能な構造として蓄積されるべきだという考えです。

このアプローチは、ホストされた質問応答システムとは異なる製品形状を MathCode に与えます。同じ研究者が使い続け、定理をキュレーションし、ローカルの形式知識の蓄積を構築するときに、その価値は増します。これは点検可能なファイルとツールチェーンの制御を求める証明エンジニアや技術的に能力のある数学者に向く可能性があります。インストール要件と Lean 中心のワークフローは初期の受け手を限定します。

形式数学はエージェントのカテゴリになりつつある

MathCode は、複数のグループが言語モデルと証明支援ツールを組み合わせようとしている分野に参入しました。HarmonicのAristotle は英語の問題を受け付け、Lean の形式化を生成し、既存の Lean リポジトリの内部で直接動作することができます。Harmonic はホストされたエージェントが最長 24 時間自律的に動作できると述べています。

Math Inc.のGauss は大規模な研究形式化を対象とし、広範な計算資源と人間の数学的指導を伴います。Math Inc. は公開評価フレームワークを備えたオープンソースのハーネスである OpenGauss もリリースしています。Axiom MathのAXLE や LeanDojo を含む研究プロジェクトは、証明生成と検証のスタックの他の部分に取り組んでいます。

MathCode はそれらのシステムに勝っていることを示す独立した証明成功ベンチマークを公表していません。公開ドキュメントはアクティブユーザー数、推論支出、自然言語の問題のうち有効な証明に到達する割合についての数字も示していません。

MathCode の擁護可能な貢献は、Zhang と Math-AI が形式証明を中心に構築することを選んだ開発者体験です。MathCode はコンパイラループ、定理の記憶、公理管理、並列計画、依存関係グラフを一つのローカル環境にまとめます。この組み合わせは、幅広い数学的信頼性を主張する以前でも、点検可能な研究システムとして有用にします。

Zhang にとって、MathCode は彼のいくつかの研究の糸をつなげます：数学的トレーニングデータの選定、推論システムの改善、モデル出力に対する厳密なチェックとしての形式検証の利用。リポジトリはその研究に対して人々が実行し、修正し、監査できるプロダクトとしての表層を与えます。次の試験は経験的なものです：蓄積された記憶が実際に利用者が難しい形式化を完成させるのに役立つか、そしてそれらの利得がますます有能になる代替手段と比較して測定できるかどうか。