Auto-formalisation avec Aristote par @HarmonicMath et ingénierie inverse avec @OpenAI GPT Codex CLI (en réalité GPT-5.2 avec xhigh et tous les avantages expérimentaux activés). En travaillant sur un exercice de l'Algèbre de Bourbaki concernant les matrices, j'ai obtenu presque 900 lignes de code Lean 4 entièrement documentées, y compris tous les détails de la preuve. J'ai ensuite passé cela - en utilisant une configuration agentique conçue à cet effet - à Codex CLI pour rétroconcevoir le fichier LaTeX correspondant, reconstruisant les étapes de la preuve directement à partir de Lean, dans le style des preuves structurées de Leslie Lamport. Ce n'est pas encore le programme de Langlands, mais nous avons besoin que ce type de mathématiques de niveau intermédiaire soit automatisé. Et cela se produit maintenant. J'ai simplement construit la bonne configuration agentique, tout pipeliné, et j'ai extrait le texte de Bourbaki (même cette partie a bien fonctionné avec @grok 4.1, ce qui est cool pour prévisualiser LaTeX en direct). Je vais finir la documentation et la publier sur GitHub. Vérifiez le graphe de dépendance - Aristote a tout géré tout seul. Et la preuve est entièrement interactive. Nous vivons maintenant dans le futur de la science !

Dans ce post communautaire, je veux mettre des liens vers des jeux très engageants et des environnements interactifs (disponibles gratuitement) qui aident les gens à explorer des concepts intellectuels en programmation et en mathématiques. Si vous connaissez d'autres endroits amusants à visiter, postez simplement ci-dessous. Amusez-vous ! Lean : Une collection de casse-têtes de programmation très engageants qui vous aident à apprendre comment les mathématiques sont prouvées et formalisées. Vous ne verrez plus jamais de la même manière la difficulté de 5*7=7*5. NandGame : Vous créez votre propre processeur à partir de zéro (même le NAND est fabriqué à partir de circuits plus simples). Hautement addictif et super amusant ! Quantum Flytrap : C'est ici que vous allez enfin comprendre les calculs quantiques. Coloré, illimité, engageant et mathématiquement très profond. Scratch : Apprenez la programmation de manière amusante. Euclidea : Apprenez à réaliser des constructions avec une règle et un compas. Cela faisait partie de l'éducation scolaire, mais maintenant c'est une application. Amusant et très informatif. Planarity : Essayez de trouver un encastrement de graphe qui montre qu'il est effectivement planaire. Golly : L'explorateur ultime des automates cellulaires. Si vous voulez approfondir : SageMath : C'est un puissant système d'algèbre informatique avec une syntaxe Python. Il est idéal pour les cours et la syntaxe de SageMath est beaucoup plus proche du discours mathématique régulier. J'aime enseigner des cours avec SageMath. GeoGebra : Vous pouvez faire des preuves, des calculs et des applets interactives. C'est une manière amusante d'apprendre de nombreux aspects des mathématiques de premier cycle. Wolfram Demonstration Projects : Une collection d'applets mathématiques qui peuvent vous aider à comprendre des sujets très sophistiqués. Vous n'avez pas besoin de Mathematica pour les exécuter, mais vous en avez besoin pour concevoir vos propres applets. The Mechanics of Proof (par Heather Macbeth) : C'est un livre avec un dépôt GitHub interactif où vous pouvez apprendre de manière plus complète la structure et la syntaxe de Lean. An Illustrated Theory of Numbers (par Martin H. Weissman) : C'est un manuel sur la théorie des nombres élémentaire avec des applications. Et ces applications sont disponibles sur le site Web sous forme de collection de Jupyter Notebooks gratuits qui vous enseignent les concepts clés. Graphical Linear Algebra : Une manière illustrée et, dans une certaine mesure, interactive d'apprendre des concepts profonds en algèbre. HomotopyContinuation.jl : C'est une manière incroyablement belle et interactive (avec Julia) d'apprendre des idées très complexes de la géométrie algébrique (composantes connexes, méthode de continuation homotopique) et avec des applications à des systèmes algébriques très spéciaux issus d'applications. Vous pouvez apprendre Julia en cours de route. Mathamaze : C'est une expérience de Helena Verrill. Géométrie magnifique, carrelages, motifs. Tout simplement merveilleux. Difficile à expliquer : n : le chemin du ninja : Si vous pensez que les mathématiques sont difficiles. Apprenez la patience de la manière difficile. Avertissement : hautement addictif. HyperRogue : Vous pouvez apprendre la géométrie hyperbolique dans un environnement de type rogue.

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