Cases
検証の実例
代表が AI のエージェントとともに書いた数理物理の論文 2 本（arXiv:2610.34122・arXiv:2610.34125、学術誌で査読中）で、何をどう確かめ、何が確かめられなかったかを書きます。 記録はすべて公開しています。
1. 論文の定数を、浮動小数を使わずに Lean で検査した
論文 II の主結果には、0.3441・0.2985・0.1252 という定数が出てきます。これらの不等式を、Lean 4 / Mathlib で、対数と π の級数による評価から証明しました。浮動小数の計算にも、計算を信じて通す命令（native_decide）にも頼っていません。
同じように、論文 I・II の証明の中の計算 23 件を形式化しました。そのうち 6 件は「論文の解析的な結果を仮定すれば、結論が出る」という含意の形で、仮定そのものは Lean では検査していません。
検査していないもの: 主定理そのもの（Fock 空間・ハミルトニアン・作用素のスペクトルは Lean に出てきません）。詳しくは 形式化のリポジトリ の「What is NOT verified」。
2. 監査をすべて通った補題に、穴が残っていた
論文 II の Lemma 8.2 は、独立した監査の層、別の AI による「穴なし」の判定、代表の通読を通って arXiv に載りました。その後、また別の AI の査読役が穴を指摘しました。指摘を監査すると、穴は本物で、ただし主張は偽ではなく修復できる、という結論でした。
ここから学んだのは、「絶対に穴がない」とは言えないということです。言えるのは、穴を無くすためにできることをやり、見つかった穴はすべて塞いだ、ということだけです。だから当社の報告では、検査の範囲と、検査していないことを必ず並べて書きます。
3. 失敗を 452 件、台帳に残した
2026-09-02 から 10-22 までに、試して閉じた方式・誤りと分かった見込み・数値計算の失敗を 452 件記録しました。何を閉じたか（方式か、標的か、命題の真偽か）を書く規則にしたので、同じ道を二度歩かずに済みました。 「原理的に不可能」と広く書いた失敗の判定が、後の監査で何度も覆ったことも記録しています。
失敗の全件の索引（公開）
4. 別の AI の「完全検証済」も、1 案ずつ確かめた
証明の簡約のために、別の AI から 52 の案を得て、1 案ずつ監査しました。本物の着想もあり、論文を軽くできたものもあります。一方で、「完全検証済」とされた 3 案のうち 1 案は誤りで、2 案は効果が主張の 1 割ほどでした。 AI の自己申告の「検証済」は、検証の代わりになりません。
5. 論文を、役割の違う読み手に採点させた
作用素論の厳密さを見る読み手、査読者、簡素化を見る読み手の 3 役を AI に割り当て、論文 2 本の計 6 人が全員 5 点満点で 4.5 を超えるまで書き直しました。初回の 3.9〜4.2 が 4.6〜4.7 になりました。これは外部の査読の代わりではなく、投稿前に読み手の目を増やす手段です。