Naukowiec opublikował pierwszą formalnie zweryfikowaną implementację operacji mesh intersection dla 3D CSG w języku Lean 4. Projekt demonstruje sposób na uniknięcie ufania kodowi generowanemu przez sztuczną inteligencję - zamiast ręcznego sprawdzania gęstego, złożonego kodu AI, człowiek musi jedynie przeczytać 93 linijki precyzyjnej specyfikacji i uruchomić formalny system dowodów Lean, który gwarantuje poprawność implementacji na etapie kompilacji.
AI pisało całą implementację oraz ponad 60 tysięcy linii formalnych dowodów w Lean, które nigdy nie wymagają inspekcji człowieka. Kompilator Lean w pełni automatycznie weryfikuje, że kod spełnia specyfikację i spełnia praktyczne warunki dobrze sformułowanej triangulacji. Podejście to jest znaczące dla bezpieczeństwa krytycznych systemów, gdzie brak zaufania do LLM jest kluczowy - zamiast wierzyć, że model napisał poprawny kod, formalny system dowodów daje matematyczną gwarancję. Projekt zawiera również demo webowe działające w WebAssembly, pokazujące praktyczne zastosowanie zweryfikowanego kernela.
To rozwiązanie otwiera nowe możliwości dla AI-assisted software engineering w domenach wymagających wysokiego poziomu pewności. Zamiast debaty o niezawodności kodu generowanego przez AI, formalista weryfikacja pozwala wykorzystać siłę generacyjnych modeli do pisania zarówno implementacji jak i dowodów, pozostawiając człowiekowi jedynie weryfikację zwięzłej specyfikacji. Dla pól takich jak kryptografia, systemy krytyczne czy geometria obliczeniowa, takie podejście może fundamentalnie zmienić sposób, w jaki ufamy AI-generowanemu oprogramowaniu.