Axiom Math a formalisé le Stacks Project pour montrer que le vibe coding à grande échelle peut être rigoureux

Axiom Math a formalisé le Stacks Project, référence centrale de la géométrie algébrique moderne, en code Lean, de sorte qu'un ordinateur peut désormais en vérifier les preuves ligne par ligne. Son essaim d'agents a travaillé comme une organisation d'ingénierie, des humains assignant des équipes à l'architecture, aux définitions centrales et aux preuves individuelles, et rien n'est entré dans la bibliothèque sans que la logique tienne. Le résultat est une bibliothèque gratuite et open source couvrant une grande partie du domaine, et un contre-exemple à l'idée que le vibe coding à grande échelle ne produit que du travail bâclé.

• Rohan Paul2026-11-04 17:53