Le problème des gros morceaux de code générés par IA n’est plus seulement de savoir s’ils compilent. C’est de savoir qui va réellement les relire.

Un projet publié par schildep pousse cette question jusqu’à la géométrie 3D. Son dépôt contient un algorithme d’intersection de maillages écrit en Lean 4, avec plus de 1000 lignes d’implémentation et environ 60 000 lignes de preuves formelles produites par des agents.

La proposition n’est pourtant pas de demander à un humain de lire tout ça. Elle est presque l’inverse : réduire ce que l’humain doit comprendre à 93 lignes de spécification, puis laisser le vérificateur de Lean contrôler que l’implémentation respecte cette spécification.

Pour quelqu’un qui travaille avec des agents, c’est un déplacement intéressant. On ne cherche plus seulement à améliorer la qualité moyenne du code généré. On cherche à réduire la quantité de code qu’il faut accepter sur parole.

Le contrat tient en 93 lignes

L’opération choisie est une intersection de solides représentés par des maillages triangulaires.

Le dépôt formalise notamment ce qu’est un maillage bien formé : surface étanche, orientation cohérente, absence de triangles dégénérés et d’auto-intersections, avec une relaxation permettant certains contacts le long d’arêtes ou de sommets.

Le cœur de la spécification dit ensuite, en substance, que le solide produit par meshIntersect doit être exactement l’intersection des deux solides d’entrée.

Ce contrat mathématique est court par rapport à l’implémentation réelle, parce qu’il n’a pas besoin d’énumérer chaque cas géométrique pénible. Sommets exactement sur une face, triangles coplanaires, intersections qui tombent sur une arête, T-junctions ou cas internes du BVH restent des problèmes d’implémentation.

Lean vérifie que l’implémentation satisfait la propriété générale.

Le développeur explique qu’un reviewer peut donc se concentrer sur quatre petits fichiers de définition, 93 lignes hors commentaires, puis lancer le checker. Les milliers de lignes générées derrière deviennent un artefact à vérifier mécaniquement plutôt qu’un texte à approuver humainement.

L’IA a aussi écrit les preuves

Le paradoxe est assez délicieux : les preuves elles-mêmes ne sont pas propres ni agréables à lire.

Le dépôt annonce environ 60 000 lignes de preuves générées par IA. Elles peuvent rester mauvaises du point de vue du style, du découpage ou de la maintenabilité. Tant que le noyau Lean les accepte sans axiome non prévu, elles démontrent ce que la spécification demande.

L’auteur va jusqu’à donner les commandes permettant d’inspecter les axiomes utilisés par les théorèmes importants et de rechercher des mécanismes comme unsafe, opaque, extern ou implemented_by qui pourraient contourner la confiance attendue.

Autrement dit, la vérification formelle ne supprime pas la question de la confiance. Elle la déplace vers une base beaucoup plus petite : le langage, son noyau de vérification, les définitions formelles et les hypothèses explicitement acceptées.

C’est plus intéressant qu’un simple « le modèle a écrit beaucoup de code ».

Le résultat est lent

Le projet ne cache pas son mauvais compromis principal.

L’intersection exacte de deux Stanford bunnies d’environ 70 000 triangles prend 24 secondes sur un M4 Pro en mono-thread, selon le benchmark du dépôt. L’auteur précise que l’implémentation est très loin des meilleurs outils de géométrie 3D.

Ce n’est pas présenté comme une limite fondamentale de Lean. Le projet utilise notamment de l’arithmétique exacte et vérifie les préconditions à l’exécution, là où des bibliothèques de production font des compromis plus agressifs avec le flottant et des structures très optimisées.

Le but ici est autre : minimiser l’effort humain nécessaire pour établir la correction.

Toutes les propriétés utiles ne sont d’ailleurs pas formalisées. Le temps d’exécution et la qualité de triangulation au-delà des conditions de bonne formation restent hors contrat. Un programme peut donc être parfaitement correct vis-à-vis de la spécification et néanmoins être lent ou produire un maillage plus fin que nécessaire.

La garantie n’est jamais « le logiciel est bon ». Elle est « le logiciel respecte précisément les propriétés que nous avons réussi à écrire ».

Un contre-test en C++ trouve trois bugs rares

Le dépôt propose aussi une comparaison instructive.

L’auteur a demandé à Claude Opus 4.8 de produire une version C++ de la même opération à partir d’une spécification informelle. Cette version a également dépassé les 1000 lignes et comportait des tests.

Un agent séparé, utilisé pour comparer le noyau C++ à la version formellement vérifiée, a identifié trois bugs distincts que l’auteur dit avoir reproduits sur des entrées spécifiques. Ils concernent des configurations géométriques rares, exactement le genre de choses difficiles à couvrir par quelques jeux de tests raisonnables.

Ce n’est pas un benchmark général opposant C++ à Lean, ni une preuve que tout code généré devrait devenir formel. C’est une expérience sur un problème qui se prête exceptionnellement bien à une définition mathématique courte et forte.

L’auteur le reconnaît lui-même : beaucoup de logiciels pratiques ne possèdent pas une spécification simple de ce type.

La nouvelle unité de revue pourrait être la spécification

Dans le développement agentique classique, l’augmentation de production crée une asymétrie gênante. Un agent peut fabriquer 5000 lignes pendant que l’humain en lit 200.

La réponse habituelle est d’ajouter d’autres agents pour reviewer les premiers. On gagne en couverture, mais on conserve une chaîne de confiance essentiellement probabiliste.

Ce projet propose une autre forme de compression : faire relire à l’humain le contrat plutôt que l’implémentation.

Ça ne marche pas partout. Ça coûte beaucoup de temps machine. Les preuves générées accumulent elles aussi de la dette. Et le contrat peut oublier une propriété importante.

Mais le changement de perspective vaut le détour. À mesure que la quantité de code devient moins chère, la ressource rare n’est plus seulement l’écriture. C’est la capacité humaine à savoir ce qu’on accepte réellement.

Ici, 93 lignes deviennent plus précieuses que 61 000.