El repositorio "verified-3d-mesh-intersection", publicado por schildep en GitHub, presenta la que su autor describe como la primera implementación formalmente verificada de una operación de geometría sólida constructiva (CSG): la intersección de mallas 3D, codificada en Lean 4 y validada contra una especificación formal de 93 líneas que define con precisión la superficie de la malla resultante y garantiza condiciones prácticas de buena formación de la triangulación.
El proyecto también funciona como experimento para no tener que confiar en código generado por inteligencia artificial. Un revisor humano solo necesita leer esas 93 líneas de especificación y ejecutar el comprobador de Lean para certificar la corrección del núcleo, sin necesidad de inspeccionar las más de 1.000 líneas de implementación escritas por la IA. Para demostrar la corrección, la IA produjo de forma autónoma más de 60.000 líneas de pruebas en Lean, que tampoco requieren revisión humana. El comprobador garantiza la conformidad con la especificación en tiempo de compilación, con confianza cero en los modelos de lenguaje.
El rendimiento es modesto: calcular la intersección exacta de dos conejos de Stanford de 70.000 triángulos cada uno tarda 24 segundos. El autor prioriza la facilidad de revisión sobre la velocidad y aclara que esa brecha no es una limitación inherente del software verificado formalmente. Incluye una demostración web que ejecuta el código compilado en el navegador, sin enviar datos a servidores, aunque la interfaz y el código de pegamento no están verificados.