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 !