Intersection de maillage CSG 3D vérifiée formellement : faites confiance à 93 lignes de spécification, pas à du code IA
Un nouveau projet, verified-3d-mesh-intersection, implémente une intersection de maillage 3D par géométrie constructive solide (CSG) formellement vérifiée en Lean 4. L'idée clé : ne faire confiance qu'à 93 lignes de spécification formelle, et non aux 1000+ lignes de code d'implémentation écrites par IA. L'IA a automatiquement écrit plus de 60 000 lignes de preuves Lean, qui n'ont jamais besoin de relecture humaine — le vérificateur Lean garantit la correction à la compilation.
Comment ça marche
La spécification définit précisément la surface du maillage résultant et garantit des conditions de bonne formation sur la triangulation. L'identité centrale :
solid (meshIntersect M1 M2) = solid M1 ∩ solid M2où solid représente l'ensemble infini des points à l'intérieur d'un maillage. Lean peut raisonner sur ces ensembles infinis et prouver l'égalité exactement.
Détails clés
- Langage : Lean 4, compilé en WebAssembly via
emcc-wasm.sh. - Performance : 24 secondes pour intersecter deux maillages de lapins de Stanford de 70 000 triangles. Lent mais priorise la vérification sur la vitesse.
- Démo web : Exécute le noyau vérifié dans le navigateur sur schildep.github.io/verified-3d-mesh-intersection. Supporte l'import STL. Aucune donnée envoyée au serveur.
- Relecture humaine : Seules les 93 lignes de spécification nécessitent une lecture. Les 1000+ lignes d'implémentation IA et les 60k+ lignes de preuves IA sont traitées comme des boîtes noires.
- Bonne formation : Si les entrées ne sont pas bien formées (par exemple, non fermées ou auto-intersectantes), l'algorithme doit détecter et signaler correctement — formalisé dans la spécification.
À qui cela s'adresse
Développeurs travaillant avec la géométrie 3D, les opérations CSG ou la vérification formelle, en particulier ceux sceptiques quant à la confiance accordée au code généré par IA sans garanties.
Architecture
Le dépôt contient le noyau Lean (CSG/), un wrapper C (wrapper.c), et du code de colle web (web/). Les commandes de construction sont fournies via lakefile.lean, emcc-wasm.sh et build_web_demo.sh. L'interface utilisateur et le code de colle ne sont pas formellement vérifiés.
📖 Lire la source complète : HN LLM Tools
👀 See Also
WSJ : Les PDG face à un choix crucial en matière d'IA – licenciements ou surcharge de travail
Le WSJ rapporte que les PDG choisissent entre licencier des travailleurs ou leur assigner plus de travail, alors que les outils d'IA promettent des gains de productivité, avec 11 points sur la discussion HN.
Concours de Protéomique Bohrium AI 2026 avec un Prix de 13 000 $ et un Soutien en Calcul
Bohrium organise une compétition d'IA en protéomique en 2026 avec un prix de 13 000 $, des opportunités de stage et un support de calcul. La compétition a été discutée sur Hacker News avec 17 points et 5 commentaires.
Discussion sur Reddit : les assistants IA réactifs critiqués, appel à une véritable proactivité
Un post sur Reddit soutient que les assistants IA actuels sont réactifs par conception, attendant des invites humaines plutôt que d'identifier proactivement les problèmes. L'auteur distingue les vérifications programmées de la véritable conscience contextuelle, notant qu'une proactivité réelle nécessite une mémoire persistante, des déclencheurs événementiels et un raisonnement temporel.
Les outils d'IA ont besoin d'une intégration pratique pour les petites entreprises, pas seulement de battage médiatique.
La communauté de l'IA se concentre sur les débats techniques tandis que les propriétaires de petites entreprises ont besoin d'outils existants intégrés à leurs flux de travail pour gérer des tâches répétitives comme la planification, les relances et la comptabilité.