Numina Lean Agent — 軽量形式定理証明エージェント

AI/ML
Numina Lean Agent — 軽量形式定理証明エージェント

Numina Lean Agent — 軽量形式定理証明エージェント

Claude Code を中核に据え、自然言語の問題記述から Lean（形式定理証明系）向けの形式化と証明を自動生成するエージェント。Putnam 競技問題の全12題を本システムで証明した実績を持ち、プロンプト設計、自己検証ループ、デモ／論文を備えた研究・実装リポジトリです。エージェント設計とLean連携のノウハウをまとめた資料（PDF）やウェブデモも提供されています。

https://github.com/project-numina/numina-lean-agent

概要

Numina Lean Agent は、Claude Code を基盤にした「形式定理証明タスク向けエージェント」です。自然言語で書かれた問題（例：Putnam 問題）を入力として受け取り、Lean などの定理証明系で検証可能な形式化と証明スクリプトを生成するワークフローを提供します。リポジトリには論文（NuminaLeanAgent.pdf）、実装の主要構成、デモ・プロンプトや設定群が含まれており、実際に Putnam の12問を本システムで解いた実績を示しています。研究用途や教育用途での自動化支援に有用です。

GitHub

リポジトリの統計情報

  • スター数: 26
  • フォーク数: 1
  • ウォッチャー数: 26
  • コミット数: 9
  • ファイル数: 9
  • メインの言語: Python

主な特徴

  • Claude Code を用いた LLM ベースのプロンプト駆動型証明生成パイプライン。
  • 自然言語→形式化→証明スクリプト生成→検証 のループで誤り検出と修正を行う自己検証機構。
  • Putnam 問題（全12問）を対象にした実証・再現可能な成果物（論文・デモ）を同梱。
  • 軽量な構成（Python ベース）で導入とカスタマイズが容易。

技術的なポイント

Numina Lean Agent の技術的な核は、大規模言語モデル（ここでは Claude Code）の出力を形式定理証明系（リポジトリ名から推測すると Lean）に結びつける「橋渡し」の設計です。具体的には、まず自然言語で与えられた定理や問題文を、LLM によるテンプレート化されたプロンプトで Lean の構文・定義に翻訳します。この過程では、定理の前提、ゴール、補題化の方針などを明示的に抽出するプロンプト設計が重要になります。生成した Lean コードは自動的に定理証明系で検証され、失敗した場合は LLM による修正版生成や局所的な戦略変更（例：分割、補題追加、誘導的証明の導入）を行う反復ループを回します。

検証のためのフィードバックには、証明系からのエラーメッセージや未解決ゴールの情報を利用し、LLM に対して「どこが失敗したか」「どの仮定が不足しているか」を具体的に伝えます。これにより、単に一次生成するだけでなく、修正を重ねて収束させる能力が高まります。また、成果の再現性を高めるためにプロンプトや設定（config ディレクトリ）を管理し、実験のログやアセットを格納する構造になっています。論文（NuminaLeanAgent.pdf）やデモサイト（Leandex、Demo）を通じて、設計思想・評価手法・具体的な証明例が示されており、研究的な検証と実用的なワークフローの両立を目指しています。

（注）リポジトリの README には「We used this system to prove all 12 problems from Put…」とあり、実問題への適用実績が明記されています。内部実装は Python を主体にしており、Claude Code の API 経由でのやり取り、プロンプトテンプレート、検証ループ、出力の整理・記録を組み合わせた設計が想定されます。

プロジェクトの構成

主要なファイルとディレクトリ：

  • .gitignore: file（不要ファイルや仮想環境、バイナリ除外設定）
  • NuminaLeanAgent.pdf: file（論文・技術報告。手法・実験結果・証明例を収録）
  • README.md: file（プロジェクト概要・導入・リンク集）
  • assets: dir（デモ用の画像や補助資料）
  • config: dir（プロンプトやAPIキー、ハイパーパラメータ等の設定）
  • …他 4 ファイル

各要素の役割（補足説明）：

  • NuminaLeanAgent.pdf: エージェントの設計原理、評価結果、Putnam 問題に対する適用例がまとまっていると推測され、実装やチューニングの参考になります。
  • config ディレクトリ: プロンプトテンプレート、モデル選択、タイムアウトや再試行回数などの運用パラメータを格納しており、実験の再現性確保や環境依存の切り分けに有効です。
  • assets: デモページや論文で使用される図、証明例スナップショットなどを格納。公開デモと連携して結果の可視化を行うための素材が含まれている可能性があります。

（リポジトリはファイル数が少なめで、主要なアルゴリズム本体は外部パッケージやデモ環境と連携している構成のようです。）

まとめ

Claude Code と Lean を結びつける実践的な自動証明エージェントの参照実装です。

リポジトリ情報：

READMEの抜粋：

Numina-Lean-Agent

Paper | Leandex | Demo | Putnam 2025

An agent built on Claude Code for formal theorem proving tasks. We used this system to prove all 12 problems from Put…