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