Formell verifizierte 3D-CSG-Netzschnittstelle: Vertraue 93 Spezifikationszeilen, nicht KI-Code

Ein neues Projekt, verified-3d-mesh-intersection, implementiert eine formal verifizierte 3D-CSG-Netzüberschneidung (Constructive Solid Geometry) in Lean 4. Die Grundidee: Vertraue nur 93 Zeilen formaler Spezifikation, nicht den 1000+ Zeilen KI-geschriebenen Implementierungscode. Die KI hat automatisch über 60.000 Zeilen Lean-Beweise geschrieben, die nie von Menschen geprüft werden müssen – der Lean-Checker garantiert die Korrektheit zur Compile-Zeit.

Wie es funktioniert

Die Spezifikation legt die genaue Oberfläche des resultierenden Netzes fest und garantiert Wohlgeformtheitsbedingungen für die Triangulation. Die Kernidentität:

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

wobei solid die unendliche Menge von Punkten innerhalb eines Netzes darstellt. Lean kann über diese unendlichen Mengen reasoning betreiben und die Gleichheit exakt beweisen.

Wichtige Details

• Sprache: Lean 4, kompiliert zu WebAssembly via emcc-wasm.sh.
• Leistung: 24 Sekunden, um zwei Stanford-Bunny-Netze mit 70k Dreiecken zu überschneiden. Langsam, aber priorisiert Verifikation vor Geschwindigkeit.
• Web-Demo: Führt den verifizierten Kernel im Browser aus unter schildep.github.io/verified-3d-mesh-intersection. Unterstützt STL-Import. Keine Daten werden an den Server gesendet.
• Menschliche Prüfung: Nur die 93-zeilige Spezifikation muss gelesen werden. Die 1000+ Zeilen KI-Implementierung und 60k+ Zeilen KI-Beweise werden als Blackboxen behandelt.
• Wohlgeformtheit: Wenn Eingaben nicht wohlgeformt sind (z.B. nicht geschlossen oder selbstüberschneidend), muss der Algorithmus dies erkennen und korrekt melden – formalisiert in der Spezifikation.

Für wen es gedacht ist

Entwickler, die mit 3D-Geometrie, CSG-Operationen oder formaler Verifikation arbeiten, insbesondere solche, die skeptisch sind, KI-generiertem Code ohne Garantien zu vertrauen.

Architektur

Das Repository enthält den Lean-Kernel (CSG/), einen C-Wrapper (wrapper.c) und Web-Glue-Code (web/). Build-Befehle werden über lakefile.lean, emcc-wasm.sh und build_web_demo.sh bereitgestellt. Die UI und der Glue-Code sind nicht formal verifiziert.