Show HN: 形式的に検証された3D CSG: 1000行のAIコードではなく、93行の仕様を信頼する

私の知る限り、これは3D構築ソリッドジオメトリ（CSG）演算、すなわちメッシュ交差の形式的に検証された最初の実装です。これはLean 4で実装され、結果のメッシュの表面を正確に特定し、三角化における実用的な正当性条件を保証する簡潔な仕様に対して検証されています。 このプロジェクトは、AI生成コードを信頼する必要性を回避するための実験でもあります。人間は93行の形式仕様を読むだけでよく、Leanチェッカーを実行することでカーネルの正しさを証明でき、AIが書いた1000行以上の複雑な実装を読む必要がありません。正しさを証明するために、AIは60,000行以上のLean証明を自律的に書きましたが、これらも人間が検査する必要はありません。Leanチェッカーはコンパイル時にLLMへの信頼を一切置かずに仕様への準拠を保証します。これにより、実装と証明をブラックボックスとして扱うことができます。私はREADMEに記載されているマイルストーンを通じてエージェントをガイドし、ここで提示されている結果に到達させました。 Webデモもご覧ください https://schildep.github.io/verified-3d-mesh-intersection/。これは、ブラウザでWebAssemblyにコンパイルされた検証済みメッシュ交差カーネルを実行します。