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

Lucrările matematice necesită validare formală. Acest lucru se face de obicei informal de către un arbitru. Dar dacă ne-am putea baza pe ceva mai robust, cum ar fi auto-formalizarea în Lean 4, unde rolul arbitrului s-ar reduce la verificarea meticuloasă a formulărilor definițiilor și teoremelor? Compilarea codului generat automat ar deveni un certificat de dovadă. Asta s-a întâmplat într-o perioadă mai lungă, așa cum am făcut cu Aristotel de @HarmonicMath. Mulțumiri lui @PietroMonticone și @llllvvuu pentru ajutorul la configurarea planului. Aici prezint o auto-formalizare corectă completă a unei lucrări a prietenului meu Stefan Barańczuk despre secvențele de divizibilitate ale lui Chebyshev. Codul conține aproximativ 5000 de linii de Lean, foarte netrivial. Corectează toate inconsecvențele și lacunele din lucrarea principală (ba chiar dovedește unele propoziții delegate). Voi posta o serie de astfel de experimente, demonstrând că în unele domenii ale matematicii, inclusiv teoria elementară a numerelor, combinatorica și analiza (tot felul de aspecte acoperite de Mathlib), nu suntem departe de o schimbare masivă în documentarea validității demonstrațiilor. Cred că va fi un an agitat!

Dacă aș fi student astăzi, interacțiunea cu LLM-uri de ultimă generație ar părea aproape ca o trișare. În această dimineață am făcut aleatoriu o poză a tablei și i-am cerut lui ChatGPT-5.2-Pro să explice contextul, soluția și câteva observații secundare despre celebra teoremă Chevalley privind mulțimile constructibile. Ceea ce am primit a fost un raport remarcabil de detaliat, care sintetiza materiale de înaltă calitate despre geometria algebrică preluate de pe internet. Aceasta ridică o întrebare serioasă: care este efortul și provocarea reală pentru studenți astăzi? Costul este cu siguranță un factor, dar odată ce accesul la aceste modele este disponibil, cum ar trebui să înveți în această țară a abundenței, unde explicațiile, referințele și explorarea interactivă sunt toate instantaneu accesibile? Poate că lupta nu mai este despre obținerea de informații sau chiar înțelegerea argumentelor individuale, ci despre dezvoltarea judecății: să știi ce întrebări să pui, ce explicații să ai încredere, cum să recunoști profunzimea versus plauzibilitatea superficială și cum să internalizezi ideile în loc să le consumi pur și simplu. Într-un mediu în care răspunsurile sunt numeroase, adevărata dificultate poate consta în formarea gustului, intuiției matematice și capacității de a naviga – mai degrabă decât de a te îneca – în acest exces brusc de cunoaștere.