Les articles mathématiques nécessitent une validation formelle. Cela se fait généralement de manière informelle par un arbitre. Mais que se passerait-il si nous pouvions nous fier à quelque chose de plus robuste comme l'auto-formalisation dans Lean 4 où le rôle de l'arbitre serait réduit à une vérification minutieuse des formulations des définitions et des théorèmes ? La compilation du code généré automatiquement deviendrait un certificat de preuve. C'est ce qui s'est passé dans une expérience plus longue que j'ai réalisée avec Aristote par @HarmonicMath. Merci à @PietroMonticone et @llllvvuu pour leur aide dans la mise en place du plan. Ici, je présente une auto-formalisation complète et correcte d'un article de mon ami Stefan Barańczuk sur les séquences de divisibilité de Chebyshev. Le code fait environ 5000 lignes de Lean hautement non trivial. Il corrige toutes les incohérences et les lacunes dans l'article principal (prouvant même certaines propositions déléguées). Je vais publier une série de telles expériences, prouvant que dans certains domaines des mathématiques, y compris la théorie des nombres élémentaire, la combinatoire et l'analyse (toutes sortes de choses couvertes par Mathlib), nous ne sommes pas loin d'un changement massif dans la documentation de la validité des preuves. Je pense que cette année va être mouvementée !