要点（30秒で）: ある開発者が、AIに書かせた1000行超の3D幾何コードを「一行も読まずに」正しいと保証する方法を示した。鍵は、人間が読むのは93行の仕様だけで、残りはLeanの証明器が数学的に裏を取るという発想。AIコードのレビュー地獄に疲れているなら、この「何を信じ、何を捨てるか」の切り分けだけでも見ておく価値がある。

この記事の内容（約9分で読めます）

1. 何が新しいのか
2. 93行に何が書いてあるのか
3. なぜ「読まなくていい」が効くのか
4. どう作られたか——AIが数万行の証明を書く
5. 反論・別の見方
6. 一人勝ちではない——競合と文脈
7. 日本・個人開発の視点
8. 要点まとめ
9. 出典・リンク

AIにコードを書かせる時代の、いちばん厄介な問題は「動くかどうか」ではない。書かれた大量のコードを、人間が本当に読み切って信用できるのか、という点だ。

その問いに、Peter Schildberger という開発者が具体的な形で答えを出した。彼が公開した verified-3d-mesh-intersection は、3Dの立体同士を掛け合わせる幾何演算を、AIに実装させつつ、その正しさを形式手法で証明したプロジェクトだ。本人いわく、3D CSG（立体を足したり引いたり交差させたりする演算）で形式検証されたのは世界で初めてだという。

何が新しいのか

普通、AIが生成したコードを信じるには、そのコードを人間が読むしかない。だが1000行あれば1000行、全部を追う必要がある。

このプロジェクトの主張は、そこを根本からひっくり返す。人間がレビューするのは4つのファイルにまたがる93行の仕様だけでいい。実装本体の1000行超も、AIが生成した6万行を超える証明も、一切読まなくてよい、と。

理由はシンプルで、正しさを保証しているのが人間の目ではなく Lean 4 という証明支援系だからだ。Leanのチェッカーがコンパイル時に「実装は仕様どおりか」を機械的に検証する。ここにLLMへの信頼はゼロで置かれている。

記事の核心「何を信じ、何を捨てるか」を一枚に。人間が読むのは93行の仕様だけ、実装1000行と証明6万行は読まず、Lean 4の証明器が「実装は仕様どおりか」を機械検証する——信頼の切り分けを示す仕組み図。

93行に何が書いてあるのか

では、その93行は何を約束しているのか。核心はたった一つの数式に近い。

solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂——ざっくり言えば「2つのメッシュを交差させた結果が表す立体は、それぞれの立体の集合としての共通部分に一致する」という宣言だ。無限個の点からなる立体を、集合として明示的に扱えるのはLeanならでは。普通のプログラミング言語では書けない性質を、あらゆる入力について証明している。

残りの仕様は、出力メッシュの「まともさ」を縛る。水漏れのない閉じた面、外向きにそろった法線、つぶれた三角形がないこと、自己交差がないこと。厳密な2-多様体までは要求せず、辺や頂点で面が触れる程度は許す——現実の3D処理が期待する条件を、過不足なく写し取っている。

そして全定理が依存する公理は、propext・Classical.choice・Quot.sound の3つだけ。Leanの標準的な土台で、独自の仮定は足していない。信じるべきものを、極限まで絞り込んでいる。

記事の対照実験を左右で比較。形式手法なしのC++はテストを3つのバグがすり抜けたのに対し、Lean 4の形式検証は「面の重なり・頂点乗り・T字接合」といった特殊ケースを原理的に封鎖する——「テストは無いことを示せない／証明は示せる」を示す比較図。

なぜ「読まなくていい」が効くのか

この設計の凄みは、Schildberger が対照実験をやってみせたところにある。

同じ機能を、今度は形式手法なしで、AIにC++で普通に書かせてみた。その1000行のカーネルに対し、別のAIエージェントたちを走らせてバグ探しをさせたところ、ユニットテストをすり抜けていた3つの異なるバグが見つかった。本人は「ブラックボックステストではまず捕まえられない」種類のバグだと書いている。

3D幾何のコードは、まさにここが地雷原だ。面が完全に重なる、頂点がちょうど別の面の上に乗る、T字の接合が生じる——こうした特殊ケースは無限にあり、ファジングでは踏み抜けない。形式検証は「あらゆる入力で成り立つ」を証明するので、この穴を原理的に塞ぐ。テストが「バグが無いことを示せない」のに対し、証明は示せる。

コードの信頼が崩れるとどれだけ厄介かは、これまでも繰り返し見てきた。スター数に釣られてスター467の「裁定ボット」は罠を掴まされる世界で、「人間の直感」に頼る保証はもう限界に近い。

プロジェクトの作られ方を上から下への処理フローに。論文のLean形式化から始め、証明付き実装→制約強化→「一般の位置」仮定の除去→加速構造の追加へと段階的に進み、各段は証明器が通るまで反復する——AIエージェントによる構築パイプライン図。

どう作られたか——AIが数万行の証明を書く

作り方そのものも今っぽい。Schildberger は主に Claude Opus 4.8 と Fable 5 を使い、24時間単位の自律セッションを何度も回して仕上げたという。

進め方は反復的で、まず単体的鎖（simplicial chains）を扱う学術論文をLeanに形式化し、基本アルゴリズムを証明付きで実装。そこから出力の制約を少しずつ強め、「一般の位置」という都合のいい仮定を外して特殊ケースを潰し、最後に高速化の加速構造を——形式的保証を保ったまま——足していった。

面白いのは、6万行を超えるLean証明を書いたのがAI自身だという点だ。人間はそれを読まない。証明器が通れば、それでいい。モデルは道具で、設定を束ねる層や検証の枠組みこそが価値を握る、という最近の潮流とも重なる。

反論・別の見方

Hacker News での議論は、称賛一色ではなかった。まっとうな疑問がいくつも投げられている。

一つは「信頼の連鎖」の話だ。LeanからCへのコード生成自体は検証されておらず、そこを保証できるのはCompCortのような限られたコンパイラだけ、という指摘が出た。これに対し「その懸念はコンパイラやハードウェアの正しさという、我々が毎日置いている前提に還元されるだけ。1000行の不透明なAIコードを信じるよりずっとマシ」という反論が返っている。実際、プロセッサそのものは検証しきれない——初期Intel 386の温度・電圧依存の乗算バグのような例もある。

もう一つは実用性だ。現状はexact rational（正確な有理数）演算を使い、GPUも使わない。7万三角形のStanford Bunny同士の交差に、M4 Proで24秒かかる。CGALのように浮動小数点の述語を信頼公理として導入すれば大幅に速くできる、と本人は道筋を示すが、いまはあくまで「正しさ優先・速度は後回し」の段階だ。

そして最も人間くさい反論がこれ。「1000行のスロップを読むほうが、93行の証明を読むより楽だ」。仕様が読める人は限られる、という現実は残る。仕様そのものが間違っていたら証明は無力だ、という根本の穴も含め、これは形式検証が昔から抱える宿題でもある。

一人勝ちではない——競合と文脈

3Dブーリアン演算の堅牢性は、この分野の長年のテーマだ。すでに Manifold というライブラリが Godot 4.4 や Blender に採り入れられ、実用の水準で「水密な」メッシュ演算を提供している。今回の成果は、それを置き換えるというより、正しさの保証を別次元に引き上げる補完的な仕事に近い。

より大きな文脈では、2026年に入って「AIコードを形式手法で裏取りする」流れが一気に太くなった。3月には Mistral が Lean 4 専用の証明エージェント Leanstral を公開し、AIが書いたコードが仕様を満たすことを証明する方向へ舵を切った。AlphaProof、DeepSeek-Prover、そして VeriBench のようなベンチマークも、Lean 4 を共通の土台に据えている。ガードレールでもテスト増産でもなく、数学的証明で信頼を作る——その一つの到達点が、今回の個人プロジェクトだ。

日本・個人開発の視点

ここで見落としたくないのは、これが大企業の研究所ではなく、一人の開発者がAIエージェントと数日回して作り上げたという事実だ。

形式検証はこれまで、専門家だけの重装備な世界だった。それを、AIに証明の大半を書かせることで個人の手に届く距離まで引き下げた。日本にもLeanやCoqを触る層は着実に増えている。「AIが書いたコードを、AIに証明させ、人間は仕様だけ守る」という分業は、少人数のチームや個人開発ほど効いてくるはずだ。読むべき93行を自分で書けるか——そこが新しい腕の見せ所になる。

要点まとめ

• 3D CSG（立体の交差演算）を世界で初めて形式検証したOSSプロジェクトが公開された。実装はAI、証明もAI、人間が読むのは93行の仕様だけ。
• 正しさを保証するのは人間の目ではなくLean 4の証明器。信じるべき公理は3つに絞られ、LLMへの信頼はゼロ。
• 同じ機能を形式手法なしでC++実装させると、テストをすり抜けた3つのバグが別のAIに発見された。証明はこの穴を原理的に塞ぐ。
• 弱点は速度（有理数演算で7万三角形が24秒）と、仕様を読める人が限られる点。信頼の連鎖はコンパイラやハードウェアにまで及ぶ。
• 2026年はLeanstralやVeriBenchなど「AIコードを形式検証する」潮流が加速。本件はその個人発の到達点。

出典・リンク

• 出典: https://github.com/schildep/verified-3d-mesh-intersection
• Hacker News（Show HN の議論）: https://news.ycombinator.com/item?id=49083239
• Manifold（比較対象のCSGライブラリ）: https://github.com/elalish/manifold
• Leanstral（MistralのLean 4証明エージェント）: https://www.startuphub.ai/ai-news/artificial-intelligence/2026/mistral-ai-s-leanstral-tackles-trust-in-code-generation
• VeriBench（Lean 4形式検証ベンチマーク）: https://openreview.net/forum?id=rWkGFmnSNl