Auto-formalizare cu Aristotle prin @HarmonicMath și inginerie inversă cu @OpenAI GPT Codex CLI (de fapt GPT-5.2 cu xhigh și toate avantajele experimentale activate). Lucrând la un exercițiu din Algebra lui Bourbaki despre matrici, am obținut aproape 900 de linii de cod Lean 4 complet documentat, inclusiv toate detaliile demonstrației. Apoi l-am trecut – folosind o configurație agentică proiectată corespunzător – către Codex CLI pentru a face inginerie inversă fișierului LaTeX corespunzător, reconstruind pașii de demonstrație direct din Lean, în stilul demonstrațiilor structurate ale lui Leslie Lamport. Acesta nu este încă programul Langlands, dar avem nevoie ca acest tip de matematică de nivel intermediar să fie automatizată. Și asta se întâmplă acum. Pur și simplu am construit configurația agentică potrivită, am făcut pipeline pentru tot și am extras textul de pe Bourbaki (chiar și acea parte a funcționat bine cu @grok 4.1, care e grozav pentru previzualizarea LaTeX live). Voi termina documentația și o voi posta pe GitHub. Verifică graful de dependență – Aristotel a gestionat totul de unul singur. Iar demonstrația este complet interactivă. Trăim acum în viitorul științei!

În această postare comunitară vreau să pun linkuri către jocuri și medii interactive foarte captivante (disponibile gratuit) care ajută oamenii să exploreze concepte sofisticate atât în programare, cât și în matematică. Dacă știi de vreun alt loc distractiv de vizitat, postează pur și simplu mai jos. Distracţie plăcută! Înclinat: O colecție de puzzle-uri de programare extrem de captivante care te ajută să înveți cum este demonstrată și formalizată matematica. Nu vei mai vedea niciodată în același mod duritatea 5*7=7*5. NandGame: Îți faci propriul procesor de la zero (chiar și NAND este făcut din circuite mai simple). Extrem de captivant și extrem de distractiv! Capcana cuantică: Aici vei înțelege în sfârșit calculele cuantice. Colorat, nelimitat, captivant și matematic foarte profund. Scratch: Învață programarea în mod distractiv. Euclidea: Învață cum să faci construcții cu riglă și busolă. Obișnuia să facă parte din învățământul școlar, dar acum este o aplicație. Distractiv și foarte informativ. Planaritate: Încearcă să găsești o încorporare de graf care să arate că este într-adevăr plană. Doamne: Exploratorul suprem de automate celulare. Dacă vrei să sapi mai adânc: SageMath: Este un sistem puternic de algebră pe calculator cu sintaxă Python. Este ideal pentru cursuri, iar sintaxa SageMath este mult mai apropiată de discursul matematic obișnuit. Îmi place să predau cursuri cu SageMath. GeoGebra: Poți face demonstrații, calcule și applet-uri interactive. Este o modalitate distractivă de a învăța multe fațete diferite ale matematicii universitare. Proiecte demonstrative Wolfram: O colecție de applete matematice care te pot ajuta să înțelegi subiecte foarte sofisticate. Nu ai nevoie de Mathematica pentru a rula, dar ai nevoie de el pentru a-ți proiecta propriile appleturi. Mecanica demonstrației (de Heather Macbeth): Este o carte cu un depozit interactiv pe GitHub unde poți învăța mai cuprinzător structura și sintaxa Lean. O teorie ilustrată a numerelor (de Martin H. Weissman): Acesta este un manual despre teoria elementară a numerelor cu aplicații. Iar aceste aplicații sunt disponibile pe site ca o colecție gratuită de Jupyter Notebooks care te învață conceptele cheie. Algebră liniară grafică: Este o modalitate ilustrată și, într-o anumită măsură, interactivă de a învăța concepte profunde în algebră. HomotopyContinuation.jl: Aceasta este o modalitate incredibil de frumoasă și interactivă (cu Julia) de a învăța idei extrem de complexe din geometria algebrică (componente conexe, metoda de continuare a omotopiei) și cu aplicații la sisteme algebrice foarte speciale care provin din aplicații. O poți învăța pe Julia pe drum. Mathamaze: Este o experiență realizată de Helena Verrill. Geometrie frumoasă, plăci, modele. Pur și simplu minunat. Greu de explicat: N: Calea Ninja: Dacă crezi că matematica este dificilă. Învață răbdarea pe calea grea. Atenție: extrem de adictiv HyperRogue: Poți învăța geometrie hiperbolică într-un mediu rogue-like.

Aici prezint o auto-formalizare completă a unei lucrări recente de matematică (din nou!) Barańczuk, Stefan. "Reducerea numărului de ecuații care definesc un subset al spațiului n-dimensional peste un corp finit." Annales de la Faculté des sciences de Toulouse: Mathématiques, ser. 6, vol. 33, nr. 1 (2024): 177–182. Am petrecut câteva zile la acest proiect. Mai întâi, am rulat Aristotele după @HarmonicMath , care în aproximativ 15 ore a auto-formalizat complet demonstrația. Apoi, cu ajutorul lui @PietroMonticone, am reușit să configurez o versiune blueprint a demonstrației. Aceasta este o versiune în care toate părțile documentației din LaTeX devin interactive și pot fi inspectate și studiate. Putem vedea dependențele din demonstrație și să studiem relațiile lor. În etapa de post-procesare, am folosit și Grok Heavy și Codex CLI cu GPT-5.2 în modul xhigh pentru a scrie o analiză linie cu linie a demonstrației formale. Acesta este un mare ajutor pentru cei care nu sunt programatori Lean 4 profesioniști. Poți cu adevărat să internalizezi toți pașii demonstrației. Vreau să rezum impresiile mele și ce am învățat din această experiență. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei