Her presenterer jeg en fullstendig autoformalisering av en nylig matematikkartikkel (igjen!) Barańczuk, Stefan. "Reduksjon av antall ligninger som definerer en delmengde av n-rommet over et endelig felt." Annales de la Faculté des sciences de Toulouse: Mathématiques, ser. 6, vol. 33, nr. 1 (2024): 177–182. Jeg brukte noen dager på dette prosjektet. Først kjørte jeg Aristoteles av @HarmonicMath, som på omtrent 15 timer fullstendig autoformaliserte beviset. Deretter, med stor hjelp fra @PietroMonticone, klarte jeg å sette opp en blåkopiversjon av beviset. Dette er en versjon der alle deler av dokumentasjonen i LaTeX blir interaktive og kan inspiseres og studeres. Vi kan se avhengighetene i beviset og studere deres relasjoner. I etterbehandlingsfasen brukte jeg også Grok Heavy og Codex CLI med GPT-5.2 i xhigh-modus for å skrive en linje-for-linje-analyse av det formelle beviset. Dette er til stor hjelp for folk som ikke er profesjonelle Lean 4-programmerere. Du kan virkelig internalisere alle trinnene i beviset. Jeg vil oppsummere mine inntrykk og hva jeg lærte av denne opplevelsen. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

Matematiske artikler trenger formell validering. Dette gjøres vanligvis uformelt av en dommer. Men hva om vi kunne stole på noe mer robust som auto-formalisering til Lean 4, hvor dommerens rolle reduseres til nøye kontroll av formuleringene av definisjonene og teoremene? Kompilering av automatisk generert kode ville bli et bevissertifikat. Dette skjedde i en lengre periode, som jeg gjorde med Aristoteles av @HarmonicMath. Takk til @PietroMonticone og @llllvvuu for hjelpen med oppsettet av blueprinten. Her presenterer jeg en fullstendig korrekt autoformalisering av en artikkel av min venn Stefan Barańczuk om Chebyshev-delbarhetssekvenser. Koden består av omtrent 5000 linjer med svært ikke-triviell Lean. Den retter opp alle inkonsistenser og hull i hovedartikkelen (og beviser til og med noen delegerte påstander). Jeg skal legge ut en serie slike eksperimenter som beviser at i noen områder av matematikken, inkludert elementær tallteori, kombinatorikk og analyse (alle slags ting dekkes av Mathlib), er vi ikke langt unna et massivt skifte i dokumentasjon av gyldigheten av bevis. Jeg tror dette kommer til å bli et hektisk år!

Hvis jeg var student i dag, ville det nesten føles som juks å samhandle med toppmoderne LLM-er. I morges tok jeg tilfeldig et bilde av tavlen og ba ChatGPT-5.2-Pro forklare konteksten, løsningen og noen sidebemerkninger om det berømte Chevalley-teoremet om konstruerbare mengder. Det jeg mottok var en bemerkelsesverdig dyp rapport, som syntetiserte materiale av høy kvalitet om algebraisk geometri hentet fra hele internett. Dette reiser et alvorlig spørsmål: hva er den virkelige innsatsen og utfordringen for studentene i dag? Kostnad er absolutt én faktor, men når tilgang til disse modellene er tilgjengelig, hvordan bør man lære i dette rikdommens land, hvor forklaringer, referanser og interaktiv utforskning er umiddelbart tilgjengelig? Kanskje handler kampen ikke lenger om å skaffe informasjon eller engang forstå individuelle argumenter, men om å utvikle dømmekraft: å vite hvilke spørsmål man skal stille, hvilke forklaringer man skal stole på, hvordan man gjenkjenner dybde versus overfladisk plausibilitet, og hvordan man internaliserer ideer i stedet for bare å konsumere dem. I et miljø hvor svarene er mange, kan den virkelige vanskeligheten ligge i å danne smak, matematisk intuisjon og evnen til å navigere – i stedet for å drukne i – denne plutselige kunnskapsoverfloden.