Jeg har personlig krysset en grense, og jeg er litt i ærefrykt. Dette er mitt første fullautomatiserte, LLM-genererte og auto-formaliserte bevis på et nytt matematisk teorem. La meg sette opp problemet: vi har tre roterende sirkler med seks posisjoner hver, alle tre krysser hverandre i totalt seks punkter. Bevis at gruppen av bevegelser de genererer er den fullstendige symmetriske gruppen S_{12}. Dette er et problem jeg opprinnelig la merke til i et nydelig puslespill i spillet Machinarium fra Amanita Design. Oppgaven er ikke ekstremt vanskelig, men den har tilsynelatende to bevis: 1. Et brute-force-søk over konjugasjonsklasser for å representere alle transposisjoner (jeg gjorde dette for mange år siden, men publiserte det aldri). 2. Et LLM-generert bevis (i dette tilfellet produsert for omtrent tre måneder siden av GPT-5-Pro), eller faktisk to bevis, begge med en briljant måte ved bruk av et teorem av Jordan om primitive grupper (eller en nært beslektet variant som er enda mer direkte). ( Det jeg manglet frem til i kveld, var et verktøy for å autoformalisere dette beviset. Takket være @HarmonicMath fikk jeg tilgang til deres bemerkelsesverdige programvare, Aristotle. Oppsummert, her er hva jeg gjorde: A. Autogenererte beviset med en LLM (og kjørte det flere ganger for å oppnå en mye forbedret versjon). B. Trimmet beviset til den rene matematiske teksten—definisjoner, proposisjoner, lemmaer, teoremer—med bevis levert av LLM. C. Kjørte Aristoteles-systemet over natten (via API). I morges mottok jeg en fullstendig formalisert versjon i Lean (omtrent 700 linjer kode). Koden kompileres, så jeg har nå et sertifikat som bekrefter at det LLM-genererte beviset faktisk førte til en korrekt løsning. Dessuten fikk jeg et konseptuelt bevis, bedre enn min egen råstyrke. Jeg planlegger å presse det videre til en bredere klasse av slike algebraproblemer. Det er et lite prosjekt, men for meg personlig markerer det en milepæl. Nå har jeg verktøy som, med min orkestrering, genuint kan hjelpe meg å oppdage, formalisere og studere bevis for matematiske teoremer. Dette er ikke trivielt. Spørsmål: 1. Hvordan vil dette skalere i fremtiden? 2. Hvor mye opplæring vil være nødvendig for å lykkes med slike oppgaver? 3. Hvordan bør vi behandle forfatterskap av slike bevis? 4. Hva er matematikernes dypere rolle?

Er det noen som planlegger å delta? Dette blir veldig gøy!

En av grunnene til at jeg ser veldig frem til nye arkitekturer, er at problemer i algebraisk topologi fundamentalt krever intuisjoner som går langt utover enkle symbolske manipulasjoner. Det er ofte mye enklere å presentere en visuell skisse av et isotopi-/homotopibasert argument enn å designe presise formler og gjøre det helt formelt. Jeg håper at en kombinasjon av verdensmodeller, symbolsk manipulasjon og representasjoner av objektdynamikk er en vei mot helt nye arkitekturer. Vi trenger dem hvis vi vil løse vanskelige matematiske problemer som går utover bare tekst. På bildet (basert på arXiv: 2107.01664) kan du se hvor lett det er å intuitivt forstå håndjernparadokset, men hvor vanskelig det ville være å skrive det formelt med formler.