形式的に検証された3D CSGメッシュ交差: AIコードではなく93行の仕様を信頼する

新しいプロジェクトverified-3d-mesh-intersectionは、Lean 4で形式検証された3D構成的立体幾何学（CSG）メッシュ交差を実装しています。重要な考え方：1000行以上のAI生成コードではなく、93行の形式的仕様だけを信頼する。AIは6万行以上のLean証明を自動生成しましたが、人間がレビューする必要はありません—Leanチェッカーがコンパイル時に正しさを保証します。

動作の仕組み

仕様は、結果のメッシュの正確な表面を特定し、三角形分割の整形式条件を保証します。核となる恒等式：

solid (meshIntersect M1 M2) = solid M1 ∩ solid M2

ここでsolidはメッシュ内部の無限点集合を表します。Leanはこれらの無限集合について推論し、等式を正確に証明できます。

主な詳細

• 言語： Lean 4。WebAssemblyにコンパイル（emcc-wasm.sh使用）。
• パフォーマンス： 7万三角形のスタンフォードバニーメッシュ同士の交差に24秒。低速ですが、検証を優先。
• Webデモ： 検証済みカーネルがブラウザで動作：schildep.github.io/verified-3d-mesh-intersection。STLインポート対応。データはサーバーに送信されません。
• 人間のレビュー： 93行の仕様のみ読めば十分。1000行以上のAI実装と6万行以上のAI証明はブラックボックスとして扱います。
• 整形式性： 入力が整形式でない場合（非閉鎖や自己交差など）、アルゴリズムは検出して正しく報告する必要があります—仕様に形式化。

対象読者

3D幾何学、CSG操作、形式検証に携わる開発者。特に、AI生成コードを保証なく信頼することに懐疑的な方。

アーキテクチャ

リポジトリにはLeanカーネル（CSG/）、Cラッパー（wrapper.c）、Webグルーコード（web/）が含まれます。ビルドコマンドはlakefile.lean、emcc-wasm.sh、build_web_demo.shで提供。UIとグルーコードは形式検証されていません。