Hoe alle wiskunde te formaliseren

De reacties van wiskundigen op de recente grote release van OpenAI variëren van enthousiasme tot frustratie, maar één ding is duidelijk: AI is opmerkelijk goed geworden in het bewijzen van stellingen, zowel formeel als informeel. De successen in het formele domein hebben ertoe geleid dat AI-enthousiastelingen verklaren dat nu het moment is om alle wiskunde te formaliseren als een nalatenschap voor toekomstige generaties.

Wij staan positief tegenover dit voorstel. We erkennen de kracht van nieuwe technologieën voor wiskundige redenering en waarderen wat zij kunnen bijdragen aan het vakgebied dat we kennen en liefhebben. Over het algemeen zijn we optimistisch over de rol die AI kan spelen, maar we maken ons ernstige zorgen over sommige recente oproepen om alles zo snel mogelijk te formaliseren. Als het goed wordt gedaan, zou een grootschalige, gecoördineerde formaliseringsinspanning de wiskundige exploratie en ontdekking enorm kunnen uitbreiden. Als het slecht wordt gedaan, zal het in het beste geval een verspilling van middelen zijn; waarschijnlijker is dat het blijvende schade aanricht.

Wij geven de voorkeur aan een kwalitatieve aanpak. Dit artikel verduidelijkt onze zorgen, beschrijft enkele van onze ervaringen met AI en formalisering, en biedt een positieve visie op hoe we kunnen werken naar een wereld waarin alle, of bijna alle, wiskundige definities, stellingen en bewijzen zijn voorzien van een formele representatie, en waarin deze artefacten de wiskunde helpen floreren.

Net zoals de rol van AI in de wiskunde tegenwoordig een gevoelig onderwerp is, geldt dat ook voor de rol ervan in formalisering. De attitudes onder expert-formaliseerders variëren sterk, net als onder wiskundigen in het algemeen. We zijn ons ervan bewust dat sommige van onze nauwste vrienden en collega's, wiens mening we zeer waarderen, sterk tegenstander zijn van grootschalige formalisering met behulp van AI. Niets van wat we hier zeggen moet worden beschouwd als representatief voor de visies van de organisaties of gemeenschappen waaraan we verbonden zijn.

De zorgen

Laten we beginnen met de observatie dat een formeel artefact weinig waard is als niemand het gebruikt. Toen Math, Inc. afgelopen februari probeerde een project te kapen om de resultaten van Maryna Viazovska over sfeerpakking in hogere dimensies te formaliseren, demonstreerde het indrukwekkend wat de technologie kon, maar daarbuiten droeg het niets bij aan de wiskunde. Het oorspronkelijke projectteam bleef werken aan een kwalitatieve formalisering van het 8-dimensionale resultaat en ontdekte al snel dat het opschonen van de door AI gegenereerde code meer moeite kostte dan het waard was; het bleek beter om de code weg te gooien en het opnieuw correct te doen, nog steeds met aanzienlijke hulp van AI.

Toen Anthropic aankondigde dat Claude de Laatste Stelling van Fermat formeel had geverifieerd met 13 miljoen regels code geschreven in 11 dagen, prees Kevin Buzzard het resultaat enthousiast, maar verklaarde tegelijkertijd dat hij niet van plan was zijn lopende formalisering van een moderner bewijs te staken. Opnieuw: hoewel de prestatie indrukwekkend is, heeft dit stuk AI-gegenereerde code waarschijnlijk weinig blijvende waarde.

Wat is hier aan de hand? De stellingen stonden niet serieus ter discussie, dus de waarde van de formele artefacten ligt uitsluitend in wat we krijgen bovenop de loutere correctheid. We willen alles formaliseren omdat we die formaliseringen willen gebruiken om méér wiskunde te bedrijven, en dat beter te doen dan we zonder deze tools zouden kunnen. We willen nadenken over mogelijke generalisaties, verbindingen tussen verschillende takken van de wiskunde verkennen en onverwachte toepassingen overwegen. We willen onze kennis herstructureren en verbeteren: een deel van het plezier van handmatige formalisering komt voort uit het besef dat we onze concepten kunnen aanpassen om ze eleganter, efficiënter en beter geschikt voor onze doeleinden te maken. Kennis is pas waardevol als het bijdraagt aan ons begrip; de waarde van een formalisering komt voort uit ons vermogen om met de data te interageren en deze te gebruiken.

Toen OpenAI oplossingen aankondigde voor de Navier-Stokes-vergelijkingen die in eindige tijd "ontploffen" (blow up), werd het natuurlijke-taalbewijs vergezeld door een Lean-formalisering. In tegenstelling tot de vorige voorbeelden speelde het correctheidssignaal hier een sleutelrol: er lijkt nu weinig twijfel te bestaan dat de oplossing correct is, ook al is het bewijs in natuurlijke taal grotendeels onbegrijpelijk. OpenAI riep desondanks de woede van de wiskundige gemeenschap op vanwege zorgen over hoe het resultaat werd verkregen, de herkomst en erkenning van ideeën, en de vrees dat de focus op louter correctheid de exploratie en het begrip ontmoedigt waar de Millennium Prize juist voor bedoeld was. Dus, zelfs hier is het onversierde formele artefact een gemengde zegen. De latere dump van OpenAI bevat verbazingwekkende en belangrijke wiskunde, maar toont tegelijkertijd een opmerkelijke minachting voor lezers en het opbouwen van begrip (sommige resultaten zijn ingetrokken, veel informele/formele paren wijken subtiel of significant uiteen, en de meeste informele beschrijvingen zijn ondoordringbaar).

Dit verklaart onze zorg. Als het besteden van miljoenen dollars aan het formaliseren van wiskunde resulteert in bibliotheken die niemand gebruikt, is dat een verschrikkelijke verspilling van middelen. Erger nog: het project zou goed onderzoek en productief gebruik van AI kunnen ontmoedigen, de sociale normen en praktijken waar onderzoek op steunt kunnen verstoren, en het vakgebied decennia terug kunnen zetten. Een grandioze mislukking zal het later moeilijk, of zelfs onmogelijk, maken om te herstellen. Een slechte formalisering van bestaande resultaten is erger dan helemaal geen formalisering.

De positieve kanten

Sommige resultaten van de grote labs zijn wel goed uitgevoerd: het werk van OpenAI aan de unit distance conjecture en het werk van Anthropic aan de dichtheid van Riemann-zeta-nulpunten vallen op. Ze demonstreerden indrukwekkende nieuwe mogelijkheden, droegen bij aan het begrip, en de gemeenschap heeft vervolgens voortgebouwd op hun werk. Dit zijn voorbeelden van hoe de labs positief kunnen bijdragen, en we nodigen uit tot verdere constructieve partnerschappen tussen de onderzoeksgemeenschap en de labs.

Goede formele bibliotheken zullen de positieve visie mogelijk maken die we hebben voor de toekomst van wiskundig onderzoek. Mensen, AI's en de taal Lean werken in concert. Tegenwoordig zijn AI's extreem bekwaam in veel aspecten van wiskundig onderzoek. Onderzoekers die interactieve stellingbewijzers gebruiken, begrijpen en waarderen al de kracht van een compiler die de geldigheid van een bewijs kan controleren. Samen zijn deze tools ongelooflijk effectief. AI's zullen formele bewijzen genereren terwijl ze werken, deze constant controleren tegen de Lean-compiler en incorrecte redeneringen automatisch wegsnoeien. Om deze visie te realiseren, hebben we een hoogwaardige, uitgebreide bibliotheek van geformaliseerde wiskunde op een ongekende schaal nodig, zodat wiskundigen effectief kunnen werken aan de frontlinie van onderzoek. Hoewel we schrijven als onderzoekswiskundigen, moeten we in gedachten houden dat deze visie verder reikt dan de wiskunde en potentieel onderzoek in techniek en wetenschap kan versnellen. Alleen als we het goed doen, zou dat resultaat een zeer grote investering van middelen rechtvaardigen.

Lessen tot nu toe

We hebben betoogd dat als we AI willen gebruiken om te helpen bij formalisering, we een speciaal geval van het alignment-probleem moeten oplossen: namelijk ervoor zorgen dat formele bibliotheken voldoen aan de wiskundige doelen van de gemeenschap. We geloven dat het oplossen van dit specifieke geval krachtige lessen zal opleveren over hoe we AI in het algemeen op een veilige, betrouwbare manier kunnen gebruiken die onze waarden ondersteunt.

Hoe kunnen we dat doen? Niemand van ons weet dat met zekerheid; dat is juist wat het leven aan de frontlinie spannend en onrustbarend maakt. Maar collectief hebben we ervaring met het gebruik van AI voor formalisering, en we verwachten dat elke serieuze inspanning aandacht besteedt aan wat we tot nu toe hebben geleerd. In het bijzonder willen we de aandacht vestigen op de volgende projecten:

  • Mathlib: Een open-source, door de gemeenschap gedreven bibliotheek die het formele wiskundige ecosysteem ondersteunt en in 2026 de Jean-Pierre Demailly Prize for Open Science in Mathematics ontving. Het wordt gecureerd door een team van 65 reviewers en inmiddels 950 bijdragers. Omdat het nadruk legt op hoogwaardige, betrouwbare code en menselijke curatie, groeit Mathlib gestaag, maar langzamer dan AI-gegenereerde bibliotheken. Om diezelfde redenen is het de primaire plek waar we leren hoe we beter kunnen formaliseren.
  • Formal Conjectures: Een collaboratieve inspanning om formele formuleringen van open problemen te verzamelen. Dit is een sociale onderneming die discussie, review en auditing vereist. AI's kunnen nuttige hulpmiddelen zijn, maar het doel is om betrouwbare formuleringen te verkrijgen van de belangrijke open vragen in diverse disciplines. We moeten projecten die formaliseringen aankondigen aanmoedigen om waar mogelijk gebruik te maken van de bestaande, getoetste formuleringen van problemen.
  • The Annals Challenge: Kevin Buzzard leidt een project om alle stellingen uit recente uitgaven van Annals of Mathematics (en later andere topbladen) te formuleren (maar niet te bewijzen). Het struikelblok hier zijn ontbrekende definities, en een van de punten van het project is dat het goede formaliseringen van definities stimuleert die in de praktijk worden gebruikt door kopstukken in het veld. Projecten als dit helpen ons de inspanningen te richten waar ze het meeste opleveren.
  • Tau Ceti: Bouwt aan een grote coherente bibliotheek van formele wiskunde, geïncubeerd door de Lean FRO en het Mathlib Initiative. Hoewel structureel vergelijkbaar met Mathlib, zijn alle bijdragen geschreven door AI's, en vervolgens adversarieel beoordeeld door andere AI's met behulp van standaard rubrieken. Deze bijdragen volgen roadmaps die zijn gecureerd door wiskundigen en formaliseringsexperts. De beoordelingscriteria omvatten passende generaliteit, het vermijden van duplicatie door hergebruik van bestaand materiaal, documentatie en naamgevingsconventies. Tau Ceti breidt Mathlib uit zonder duplicatie en volgt alle daar gemaakte ontwerpbeslissingen. Het is mogelijk om bij te dragen aan Tau Ceti door roadmaps te schrijven of door inferentie te leveren. Tau Ceti is nu iets groter dan Mathlib (3 miljoen regels code) en groeit snel. Recente resultaten omvatten Riemann-Roch, Schur-Weyl dualiteit, Jordan-Brouwer separatie, Rellich-Kondrakov compactheid en Chebotarev-dichtheid.
  • Formal Frontier: Een project van het Mathlib Initiative dat een pipeline bouwt die bronteksten omzet in onderling verbonden formele bibliotheken. Het maakt gebruik van een interagerende gemeenschap van AI-agenten die kunnen worden geïnstrueerd om specifieke teksten te formaliseren. Dit systeem is ontworpen met schaalbaarheid in het achterhoofd, zodat het duizenden tekstboeken kan verwerken. Er zijn nu 41 gepubliceerde bibliotheken (bijv. over profinite groepen, torische idealen en homologische algebra) bestaande uit ongeveer 200.000 regels code. Naast het leveren van infrastructuur voor het beheer van de agent-zwerm, heeft het Formal Frontier-project een build-server geschreven voor grote Lean-projecten. Recente hoogtepunten zijn formaliseringen van de hairy ball theorem, de stelling van Kaplansky over projectieve modules, de stable range theorem van Bass, Tate-periodiciteit en Stone-dualiteit voor spectrale ruimten.

Zowel Formal Frontier als Tau Ceti maken gebruik van agenten en adversariële review, maar ze verschillen in hun aansturing en outputstructuur. Tau Ceti gebruikt roadmaps gecureerd door experts en bouwt één enkele coherente bibliotheek. Formal Frontier is primair een source-to-library pipeline. Beiden stellen dat een formalisering alleen waardevol is als anderen erop kunnen voortbouwen. We verwachten dat toekomstige autoformaliseringsprojecten op beide benaderingen zullen voortbouwen.

  • Palomar: Een online register van formele wiskundeprojecten. Het doel van Palomar is om formaliseringsprojecten te indexeren die gericht zijn op specifieke resultaten, maar niet noodzakelijkerwijs streven naar deelname aan een algemene bibliotheek. Veel van deze resultaten zijn onlangs op GitHub "gedumpt", en het kan zeer moeilijk zijn ze te interpreteren of te vertrouwen. Palomar lost dit probleem op door twee kenmerken te vereisen voor elk project dat het indexeert:
  1. Het project moet een formalization.yaml-bestand bevatten; een metadata-bestand met een zelfbeoordeling van wat is geformaliseerd, hoe het is gedaan (bijv. uitsluitend door mensen, in samenwerking met AI's, of autonoom door AI's), en ook de relaties met ander werk en hoe de auteurs van het onderliggende informele onderzoek betrokken waren.
  2. Het project moet een Comparator-setup bevatten, wat het makkelijker maakt om precies te auditeren wat de stelling bewijst.

Mathlib, Tau Ceti en Formal Frontier streven naar gemeenschappelijke waarden. Deze zijn niet specifiek voor autoformalisering, maar zijn principes die gelden voor alle formele bibliotheken. De Mathlib-gemeenschap heeft onlangs een document over waarden gepubliceerd, en dat is het startpunt voor onze eigen lijst:

  • Vertrouw op door mensen gecureerde bibliotheken, in het bijzonder Mathlib; volg hun ontwerpprincipes en coderegels, en refactor continu om hun beslissingen over te nemen.
  • Geef de voorkeur aan grondigheid en breedte. Deze moeten voorafgaan aan diepgang, maar maken die uiteindelijk wel mogelijk.
  • Vermijd duplicatie. Generaliseer stellingen voor maximaal hergebruik.
  • Review toevoegingen publiekelijk, volgens overeengekomen standaarden.
  • Publiceer vrij. Bibliotheken moeten open source, interoperabel en exploreerbaar zijn.
  • Blijf up-to-date. Zorg voor continue compatibiliteit met elke release van Lean en Mathlib.
  • Blijf openstaan voor veranderingen. Als er een betere aanpak wordt ontdekt, is het nooit te laat.
  • Documenteer en organiseer. Bestanden moeten coherent en systematisch georganiseerd zijn, en hun inhoud moet gedocumenteerd zijn.
  • Link naar de bestaande literatuur. Een wiskundige moet kunnen vertrouwen op en verifiëren dat de concepten in de bibliotheek de verwachte betekenis hebben.
  • Stel standaarden vast en voldoe eraan. Het produceren van laagwaardige of niet-geauditeerde code en beweren of hopen dit "later op te schonen" is contraproductief.

Mathlib implementeert deze waarden via het reviewproces en community-discussies. Tau Ceti en Formal Frontier implementeren deze waarden in de code en prompts die hen aansturen, evenals in door de gemeenschap geschreven planningsdocumenten.

De weg vooruit

Binnen drie jaar, en mogelijk veel eerder, kan het grootste deel van de wiskunde zodanig worden geformaliseerd dat wiskundigen formele bibliotheken kunnen verkennen, erop kunnen voortbouwen en ze kunnen gebruiken. Dit zou ons vermogen om nieuwe wiskunde te ontwikkelen en te ontdekken aanzienlijk uitbreiden. De Lean FRO is toegewijd aan het waarborgen dat Lean projecten op deze schaal kan ondersteunen. Het behalen van dit ambitieuze project vereist verschillende soorten aanvullende ondersteuning en deelname van de gemeenschap:

  1. Cureer en draag bij aan Mathlib, het fundament van het formele wiskundige ecosysteem, waar we best practices in formalisering ontdekken.
  2. Lever de benodigde middelen voor de projecten die klaarstaan voor uitvoering, Tau Ceti en Formal Frontier, zodat deze in enkele maanden tijd met een factor tien kunnen groeien.
  3. Schrijf de expert-roadmaps en blauwdrukken die de implementatie van grote formele bibliotheken begeleiden. Stel workshops voor en ondersteun deze om vakspecifieke bibliotheken te ontwerpen en te verbeteren.
  4. Ontwikkel geloofwaardige modellering van de financiële, technische en engineering-vereisten voor opschaling.
  5. Pleit voor controle door wiskundigen over de tools en middelen die nodig zijn voor autoformalisering.
  6. Lanceer non-profit of academische hosting voor de wiskundigen, ingenieurs en inferentie die nodig zijn voor de implementatie van grootschalige formalisering, inclusief de nodige governance en adviesorganen.

***

Voetnoten:

  1. Iedereen kan helpen bij het bouwen van Tau Ceti door het volgende uit te voeren:

uv tool install git+https://github.com/TauCetiProject/TauCetiWorker gevolgd door tauceti work --loop (Hiervoor zijn claude of codex nodig, en de gh GitHub command line tool met authenticatie.)

  1. Dit gebeurt al, bijvoorbeeld tijdens bijeenkomsten over statistiek en fysica bij ICARM, analyse bij ICERM, en PDE's bij SLMath.
  2. We zijn van plan om modellen gebaseerd op Tau Ceti en Formal Frontier zo snel mogelijk te leveren, maar dit valt buiten de scope van een blogpost.