Ces dernières années, le domaine a connu des avancées importantes. Des mathématiciens de premier plan, comme Terence Tao et Peter Scholze, intègrent désormais ces outils dans leurs recherches, contribuant à leur diffusion au sein de la communauté scientifique. Parallèlement, les assistants de preuve sont devenus plus puissants et plus accessibles, tandis que l’intelligence artificielle ouvre de nouvelles perspectives pour automatiser certaines étapes de la formalisation.
Un exemple : l’empilement de sphères
Le problème de l’empilement de sphères cherche à déterminer comment organiser des sphères pour occuper un espace de manière optimale. Une disposition simple en grille laisse apparaître des espaces vides importants. En revanche, une disposition décalée, semblable à celle d’oranges sur un étal, permet d’utiliser l’espace de manière plus efficace.
Dès 1611, Johannes Kepler avait formulé l’hypothèse selon laquelle cette configuration est optimale en trois dimensions. Il a fallu attendre 1998 pour que Thomas Hales en apporte la démonstration, ensuite vérifiée à l’aide d’un assistant de preuve. En 2016, Maryna Viazovska a résolu le problème analogue en huit dimensions, une avancée majeure qui lui a valu la médaille Fields en 2022.
Humains et intelligence artificielle : une collaboration prometteuse
Plus récemment, une équipe internationale réunissant des spécialistes de Suisse, du Royaume-Uni et des États-Unis a réussi à formaliser les résultats de Viazovska à l’aide de l’assistant de preuve Lean. Une part importante du travail a été réalisée grâce à l’intelligence artificielle : certaines étapes ont été générées automatiquement par « Gauss », un modèle de langage développé par l’entreprise Math, Inc..
À l’occasion de l’atelier « Formalization and Proof Assistants » (25–27 mars 2026), organisé par le professeur David Loeffler à UniDistance Suisse, des expertes et experts présenteront les développements récents du domaine. Maryna Viazovska fera également partie des intervenants, Maryna Viazovska. L’événement se tiendra en parallèle de la rencontre de printemps de la Société mathématique suisse.
La Diligentia Foundation soutient un projet de recherche d’UniDistance Suisse sur les obstacles administratifs dans le système fiscal
Économie Lire la suite
«UniDistance Suisse est une institution attrayante dans le domaine de la recherche scientifique de haut niveau»
Économie Lire la suite
