Résumé
Dans cet exposé, nous discuterons de l’état actuel de la formalisation de la théorie des nombres moderne dans mathlib, la bibliothèque mathématique de Lean. Nous mettrons en avant les avancées récentes, les principaux défis qui ont été relevés, ainsi que les implications plus larges de ce travail. Nous aborderons également les perspectives d’avenir et les applications potentielles, en soulignant comment ces développements contribuent à l’écosystème croissant des mathématiques formalisées.