Voici une auto-formalisation complète d'un récent article de mathématiques (encore une fois !) Barańczuk, Stefan. "Réduire le nombre d'équations définissant un sous-ensemble de l'espace n sur un corps fini." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024) : 177–182. J'ai passé quelques jours sur ce projet. Tout d'abord, j'ai utilisé Aristotle par @HarmonicMath, qui en environ 15 heures a complètement auto-formalisé la preuve. Ensuite, avec l'aide précieuse de @PietroMonticone, j'ai réussi à mettre en place une version de base de la preuve. C'est une version dans laquelle toutes les parties de la documentation en LaTeX deviennent interactives et peuvent être inspectées et étudiées. Nous pouvons voir les dépendances dans la preuve et étudier leurs relations. Au stade de post-traitement, j'ai également utilisé Grok Heavy et Codex CLI avec GPT-5.2 en mode xhigh pour écrire une analyse ligne par ligne de la preuve formelle. C'est une grande aide pour les personnes qui ne sont pas des programmeurs professionnels de Lean 4. Vous pouvez vraiment internaliser toutes les étapes de la preuve. Je veux résumer mes impressions et ce que j'ai appris de cette expérience. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

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 !

Si j'étais étudiant aujourd'hui, interagir avec des LLM à la pointe de la technologie semblerait presque être de la triche. Ce matin, j'ai pris au hasard une photo du tableau noir et j'ai demandé à ChatGPT-5.2-Pro d'expliquer le contexte, la solution et quelques remarques sur le célèbre théorème de Chevalley sur les ensembles constructibles. Ce que j'ai reçu était un rapport remarquablement approfondi, synthétisant du matériel de haute qualité sur la géométrie algébrique tiré de l'ensemble d'internet. Cela soulève une question sérieuse : quel est l'effort réel et le défi pour les étudiants d'aujourd'hui ? Le coût est certainement un facteur, mais une fois l'accès à ces modèles disponible, comment doit-on apprendre dans ce pays d'abondance, où les explications, les références et l'exploration interactive sont toutes instantanément accessibles ? Peut-être que la lutte n'est plus d'obtenir des informations ou même de comprendre des arguments individuels, mais de développer un jugement : savoir quelles questions poser, quelles explications faire confiance, comment reconnaître la profondeur par rapport à la plausibilité superficielle, et comment internaliser des idées plutôt que de simplement les consommer. Dans un environnement où les réponses sont abondantes, la véritable difficulté peut résider dans la formation du goût, de l'intuition mathématique et de la capacité à naviguer - plutôt que de se noyer dans - cet excès soudain de connaissances.