Actualités Agenda
Des diplômes universitaires en ligne qui s'adaptent à votre vie et à votre carrière
Bachelor Master Doctorat
Étudier à distance Admissions et inscriptions Ressources pour étudiants Campus en ligne
Formation continue
Alumnae et alumni
Evènements pour étudiants
Découvrez nos travaux académiques et rencontrez nos chercheurs
Groupes de recherche Projets de recherche Leçons inaugurales Campus de recherche Brigue
Coup de projecteur sur la recherche Collaborations internationales Early-career researchers
Publications
Chercheuses et chercheurs
Evènements scientifiques
Des opportunités d'apprentissage ouvertes à toutes et à tous
Uni60+ Auditeurs et auditrices libres
Formations pour les entreprises Mandats de consulting Exemples de prestations
Evènements grand public
Découvrez notre institution et collaborez avec nous
Portrait Stratégie Reconnaissance Espace media Travailler à UniDistance Suisse
Faculté de droit Faculté de psychologie Faculté des sciences économiques Faculté d'histoire Faculté de mathématiques et informatique
Organisation
Cadre réglementaire
Contact

SMS Spring Meeting : Formalisation et assistants de preuve

La formalisation des preuves mathématiques consiste à traduire des raisonnements rédigés par des humains dans un langage formel précis, compréhensible par un ordinateur. Cette démarche permet de vérifier rigoureusement la validité des démonstrations. Elle reste toutefois exigeante, car elle nécessite une compréhension approfondie des mathématiques ainsi que du système formel utilisé. Les outils informatiques qui accompagnent ce processus sont appelés assistants de preuve.

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

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.