axiom-verify

Axiom Lean 4 による証明検証

Axiom は、Axle API を通じてクラウドベースの Lean 4 証明検証を提供します。ローカルに Lean をインストールしなくても、完全な Mathlib 環境で Lean コードをコンパイルしてチェックできます。検証結果は、ローカルでビルドするのに数分かかるところ、数秒で返ってきます。

初回使用前

Axle コマンドを実行する前に、セッションごとに以下を一度確認してください。

1. API キー：echo $AXLE_API_KEY を実行します。空の場合は、ユーザーが axle.axiommath.ai/app/console からキーを取得し、export AXLE_API_KEY=<key> で設定する必要があります。
2. CLI のインストール：axle --version を実行します。見つからない場合は、pip install axiom-axle でインストールします。
3. Lean 環境：Lean のバージョンを確認するため、プロジェクトのルートに lean-toolchain ファイルがあるか確認します。存在する場合は、そのバージョンを使用します（例：leanprover/lean4:v4.28.0 は lean-4.28.0 になります）。存在しない場合は、デフォルトの lean-4.28.0 を使用します。

参考ファイル

タスクに応じて、必要なファイルを参照してください。

1. references/axiom-configuration.md -- セットアップ、認証、環境の選択について説明します。ユーザーがまだ Axiom を設定していない場合は、最初に読んでください。
2. references/axiom-api-reference.md -- 14 個すべての API エンドポイントと、パラメーターおよびレスポンス形式について説明します。正確なパラメーター名やレスポンスフィールドが必要な場合に読んでください。
3. references/axiom-cli-reference.md -- CLI コマンドとオプションについて説明します。ローカルファイルを扱う際に、正確なフラグや使用方法の詳細を確認するために読んでください。
4. references/axiom-best-practices.md -- ワークフローの指針、結果の解釈、注意点、ヒントについて説明します。複数ステップのワークフローを計画するときや、予期しない動作が発生したときに読んでください。
5. references/agents/verify-fix-agent.md -- 自律的なチェック → 修正 → 検証のワークフローを行うエージェントです。
6. references/agents/clean-analyze-agent.md -- 自律的な正規化 → 抽出 → クリーンアップ → チェックのワークフローを行うエージェントです。

ワークフロー

ステップ 1：適切なツールを選択する

ユーザーの意図に合ったエンドポイントを選択します。

ユーザーの目的	エンドポイント	備考
証明が正しいか検証する	verify_proof	候補の証明を形式的な命題に照らしてチェックします
コードがコンパイルできるか確認する	check	構文と型をすばやくチェックします
証明の構造を把握する	extract_theorems	ファイルを自己完結した定理単位に分割します
宣言名を変更する	rename	全体を通じて参照を自動更新します
定理／補題を変換する	theorem2lemma	theorem と lemma のキーワードを切り替えます
証明をスタブ化する	theorem2sorry	足場として、証明を sorry に置き換えます
ファイルを結合する	merge	ファイル間でインテリジェントに重複を排除します
何もしないタクティクや have を削除する	simplify_theorems	証明状態を変更しないタクティクや、未使用の have を削除します
完了後のタクティクを削除する	repair_proofs	証明完了後のタクティクを削除し、sorry を置き換え、安全でないタクティクを修正します
have 文を抽出する	have2lemma	インラインの have を独立した補題に昇格させます
have の本体をスタブ化する	have2sorry	have の本体を sorry に置き換えます
sorry のプレースホルダーを抽出する	sorry2lemma	sorry を補題のスタブに変換します
命題が偽かどうかを検証する	disprove	Plausible を使用して反例を試みます
書式を標準化する	normalize	セクション、名前空間、コメントを整理します

どのツールを使うべきか判断できない場合は、次の手順で進めてください。

• まず check を使い、コードがコンパイルできるか確認します
• extract_theorems を使い、ファイルの内容を把握します
• ファイルで section／namespace ブロックを使っている場合は、最初に normalize を使います（これらのブロックは他のツールで問題を起こすことがあります）

ステップ 2：実行

ローカルファイルを扱う場合は、axle CLI を優先してください。ディスクから直接ファイルを読み込み、構文がよりシンプルで、-o を使って出力をファイルに書き込めます。CLI は環境変数から AXLE_API_KEY を自動的に読み込みます。注意：CLI コマンドではハイフン（例：verify-proof）を使いますが、HTTP API ではアンダースコア（verify_proof）を使います。すべてのコードは、完全な Mathlib 環境でコンパイルするために axle.axiommath.ai に送信されます。CLI による検証はローカルでは行われません。

Lean コードを動的に構築する場合（スクリプトや CI/CD パイプラインでコンテンツを生成する場合、またはプログラムからコード文字列を組み立てる場合）は、curl または Python クライアント（pip install axiom-axle）を介して HTTP API を使用してください。API はコンテンツを JSON 文字列として受け取るため、生成したコードやメモリ上のコードに適しています。

コードがコンパイルできるか確認する：

axle check file.lean --environment lean-4.28.0 --ignore-imports

証明を検証する：

axle verify-proof formal_statement.lean proof.lean \
  --environment lean-4.28.0 --ignore-imports

壊れた証明を修復する：

axle repair-proofs file.lean --environment lean-4.28.0 --ignore-imports \
  --repairs remove_extraneous_tactics,apply_terminal_tactics

予想を反証する：

axle disprove file.lean --environment lean-4.28.0 --ignore-imports

ファイルを正規化する（セクション／名前空間をフラット化する）：

axle normalize file.lean -o normalized.lean --environment lean-4.28.0 --ignore-imports

定理を抽出する：

axle extract-theorems file.lean --environment lean-4.28.0 --ignore-imports

定理を簡略化する：

axle simplify-theorems file.lean --environment lean-4.28.0 --ignore-imports

宣言名を変更する：

axle rename file.lean --declarations '{"old_name": "new_name"}' \
  --environment lean-4.28.0 --ignore-imports

証明を sorry でスタブ化する：

axle theorem2sorry file.lean --environment lean-4.28.0 --ignore-imports

変換結果をファイルに書き込む（normalize、repair-proofs、simplify-theorems、rename などで利用可能）：

axle normalize file.lean -o output.lean -f --environment lean-4.28.0 --ignore-imports

API の例（動的に構築したコード向け）：

curl -s -X POST https://axle.axiommath.ai/api/v1/check \
  -H "Authorization: Bearer $AXLE_API_KEY" \
  -H "Content-Type: application/json" \
  -d "$(jq -n \
    --arg content "$LEAN_CODE" \
    '{content: $content, environment: "lean-4.28.0", ignore_imports: true}')" \
  | jq '{okay, failed_declarations, lean_errors: .lean_messages.errors, tool_errors: .tool_messages.errors}'

CLI コマンドの全リファレンスについては、references/axiom-cli-reference.md を参照してください。14 個すべてのエンドポイントの API パラメーターに関する全リファレンスについては、references/axiom-api-reference.md を参照してください。

ステップ 3：結果を解釈する

すべての応答には、Lean コンパイラーの出力である lean_messages と、Axle の診断情報である tool_messages が含まれます。必ず両方を確認してください。変換ツールでは、tool_messages にエラーがなく成功しているように見えても、lean_messages.errors にコードがコンパイルされなかったことが示される場合があります。

エンドポイントの種類（check、verify_proof、変換ツール、disprove）ごとの結果の詳しい解釈、user_error の応答形式、重大度レベルについては、references/axiom-best-practices.md をお読みください。

重要： インポートを正確にテストする場合を除き、常に --ignore-imports ／ "ignore_imports": true を使用してください。これを指定しないと、インポートの不一致によって標準的な応答ではなく user_error が返されます。

よくある複数ステップのワークフロー

証明を検証して修正する： references/agents/verify-fix-agent.md に従うエージェントを起動します。エージェントは check → repair → 再チェック → verify を自動的に実行し、構造化された診断結果を返します。

ファイルを分析して整理する： references/agents/clean-analyze-agent.md に従うエージェントを起動します。エージェントは normalize → extract → repair → simplify → check を自動的に実行し、整理済みの出力と構造の概要を返します。

証明の開発を準備する：

1. 形式的な命題を書く
2. theorem2sorry — 証明を sorry でスタブ化する（特定の定理を対象にするには names パラメーターを使用）
3. 証明を段階的に埋める
4. 各証明の後に check を実行して進捗を確認する
5. sorry2lemma — 残っている義務を追跡する（{name}.sorried という補題のスタブを生成し、sorry を含む各定理の前に挿入します）
6. 最終検証に verify_proof を使用する

予想をテストする：

1. disprove — まず反例を探す
2. 反例が見つからなければ、証明を試みる
3. 証明を作成しながら、段階的に check を実行する
4. 完成したら verify_proof を実行する

よくある落とし穴

コードを送信する前に、references/axiom-best-practices.md をお読みください。主な注意点：独自の属性は取り除く必要があります。Mathlib では autoImplicit が無効です。名前のシャドーイングは気付かれない失敗の原因になります。セクションや名前空間を含む場合は、先に normalize が必要です。また、コンパイルエラーがあると、変換ツールは変更のない内容をエラーなしで返します。