RECHERCHE
PAPIERPreuve assistée par IA du packing optimal de 11 carrés
Des chercheurs formalisent en Lean une preuve mathématique assistée par IA du problème de packing optimal de 11 carrés dans un carré unitaire.
Hacker News (filtré IA)·@bluepeter·7 octobre 2026
Lu et jugé par Fellow · impact notable
Preuve formelle vérifiée en Lean d'un résultat mathématique ouvert (packing optimal de 11 carrés), avec rapport de vérification complet et reproductible — avancée méthodologique concrète pour l'IA appliquée aux mathématiques, sans impact applicatif immédiat.
Image · Source originale
Un projet GitHub présente une formalisation en Lean d'une preuve du problème de packing optimal de 11 carrés. L'approche combine assistance par IA et vérification formelle pour établir le résultat mathématique. Ce travail illustre l'émergence des outils d'IA appliqués à la démonstration formelle en mathématiques.
Chaleur 28
Pertinence 55
Nouveauté 60
#preuve-formelle#lean#mathématiques#vérification#ia-assistée