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.
