axiom-explorer: un experiment honest en descobriment matemàtic assistit per LLM

El primer preprint d’un petit experiment meu ja és a Zenodo. El preprint descriu una eina que vaig construir —no un teorema que vaig demostrar— i el workflow que implementa. Et vull explicar de què va sense la retòrica habitual sobre la intel·ligència artificial resolent les matemàtiques, perquè l’experiment és més modest que això i la seva honestedat és precisament la part que crec que val la pena compartir.

La pregunta

Hi ha una tensió persistent en matemàtiques entre la velocitat amb què es produeixen idees fundacionals noves i la velocitat amb què la comunitat pot explorar les seves conseqüències en altres branques. Quan apareix un marc axiomàtic fresc —la matemàtica condensed el 2019, el programa de la dualitat sintètica de Stone el 2024— passen anys fins que la pol·linització creuada amb altres branques cristal·litza en resultats citables. La major part d’aquest temps no se’n va en proves difícils, sinó en la feina més senzilla de descobrir on dues comunitats parlen calladament del mateix amb vocabularis distints.

La pregunta és si un workflow acurat i ben acotat pot fer part d’aquesta feina de descobrir-on i presentar els resultats com a invitacions falsables a revisió experta.

L’instrument

axiom-explorer és aquest instrument. És un harness en Python amb un grapat d’eines externes (arXiv, Mathlib4, Z3, SymPy, Lean 4, latexmk) i un model de llenguatge gran com a orquestrador. L’orquestrador és la part que més probablement posa nerviosa la gent —raonablement— i el disseny de l’eina consisteix en gran mesura a restringir què pot fer l’orquestrador.

El workflow corre en cinc fases:

1. Mapeig bibliomètric. El harness tria un conjunt petit de “llavors axiomàtiques modernes i productives” de branques distintes —en aquesta corregüda: l’axioma d’univalència de la teoria de tipus homotòpica, la matemàtica condensed, els espais perfectoides, i la curvatura de Ricci sintètica— i consulta arXiv en les seves combinacions per parells fent servir cinc estratègies de cerca distintes. La sortida és una puntuació de densitat per parell.
2. Inventari de l’estat formal. Per a cada llavor, el harness escaneja la biblioteca Mathlib4 i projectes adjacents a Lean i Agda, comptant fitxers, definicions, i TODOs explícits.
3. Dossiers per parell. Per als parells que sobreviuen a la Fase 0, construeix un dossier integrant literatura, functors pont, i experiments numèrics o simbòlics a petita escala.
4. Immersió profunda. Els candidats que sobreviuen als dossiers es promouen al seu propi dossier amb enunciat precís, evidència, i un nivell de confiança explícit en una escala de quatre nivells.
5. Síntesi i informe. Els candidats supervivents i la meta-anàlisi metodològica esdevenen un esborrany de preprint que després s’itera contra diverses rondes de revisió per parells mitjançant IA abans que s’apropi a cap revisor humà.

L’escala de confiança

Cada afirmació que el harness fa emergir porta una etiqueta:

• L0 — verificat mecànicament. Z3 no va trobar contraexemple. Lean type-comprova els axiomes.
• L1 — fort. Un resultat estàndard i citat, amb referència.
• L2 — plausible. Argumentat pel workflow, no verificat directament.
• L3 — especulatiu. Una conjectura que emergeix de la cerca creuada, registrada com a pregunta, mai com a afirmació.

Aquest és el dispositiu de protecció descendent més important. És la diferència entre un preprint que promet certesa a l’estil folklore i un que entrega al lector exactament el nivell de confiança que el workflow s’ha guanyat.

Les stop rules

L’orquestrador té quatre stop rules dures que el workflow es nega a saltar-se:

• No publica a Zenodo ni a cap altre lloc sense que l’autor humà premi explícitament el botó de publicar.
• No envia correus electrònics ni cap altra comunicació externa; els esborranys es produeixen, l’autor humà els despatxa.
• No reclama novetat més enllà d’una forma molt estreta: “aquesta formulació no apareix com a tal en cap font única que hàgim trobat”.
• No suplanta autoritat matemàtica. La identitat de l’autor i el mètode de producció assistit per LLM es declaren a la portada de cada preprint que surt.

Aquestes es comproven als punts de revisió de codi. El harness es nega a marcar un candidat com a “llest” fins que l’escala de confiança està omplerta i la disclosure està al seu lloc.

El bucle de revisió per parells amb IA

Aquesta és la part que més em va sorprendre durant l’experiment. L’esborrany de la Fase 5 se sotmet a diversos revisors LLM distints (famílies de model distintes, prompts distints) abans de cap revisió humana. Cada ronda produeix una crítica estructurada que l’orquestrador ha d’abordar punt per punt, amb retractació explícita de qualsevol afirmació anterior que la revisió hagi demostrat equivocada.

En el cas d’estudi que vam executar, quatre rondes de revisió per parells amb IA (v1→v1.1, v1.1→v1.2, v1.2→v1.2.1, v1.2.1→v1.2.2) van agafar tres errors matemàtics substantius que l’esborrany original contenia:

• Una fallada d’invariància en un invariant de mida clau.
• Una cota de cardinalitat sobre grups profinits lliures expressada en una forma inconsistent amb les atestacions geomètriques que es citaven.
• Un exemple model-teòric que jo havia classificat com a trivial quan en realitat és el grup de Galois absolut dels racionals.

Una cinquena ronda va agafar un error de citació (un identificador d’arXiv que apuntava a un paper sobre turbulència en lloc del treball previst sobre grups de Lascar). Cap d’ells hauria estat caçat per una sola generació LLM. Tots van ser caçats abans que s’apropés cap revisor humà expert.

El bucle no substitueix la revisió experta. És, però, una primera línia de defensa notablement barata i eficaç.

El cas d’estudi, breument

Vaig fer córrer el workflow sobre una quàdruple de llavors. El que va sortir és el tema d’un segon preprint a part —el paper conjectural acompanyant, forthcoming— que dipositaré amb el seu propi DOI els pròxims dies. El resum curt és que el harness em va dirigir a dos papers recents i cridaners que no havia llegit amb cura (el treball de Haine et al. sobre el tipus d’homotopia condensed d’un esquema, i el propi paper de Haine de 2026 que unifica el grup fonamental proétale d’un esquema amb el grup de Lascar d’una teoria completa de primer ordre), i llegir-los junts suggeria una envoltant cardinal candidata que, fins on vaig poder comprovar, no apareix escrita en cap font única.

Aquest candidat es presenta com una conjectura falsable, amb etiquetes de confiança explícites, i el preprint acompanyant és una invitació oberta a especialistes en matemàtica condensed, teoria de models i teoria de conjunts a fer exactament el que els especialistes fan: confirmar-la com a folklore, trobar un contraexemple, o refinar-la. Qualsevol dels tres és un resultat excel·lent.

El que crec que val l’experiment

No sóc un matemàtic amb doctorat. Treballo a la frontera entre l’enginyeria de programari i els mètodes formals, i no tinc res a fer escrivint sobre $\infty$-topoi sense ajuda explícita. La primera cosa que fa el workflow és deixar això obvi en cada artefacte que produeix.

El que sí crec que val l’experiment, en el seu àmbit correcte, és:

• És honestament publicable com a observació registrada, amb un DOI, precisament perquè el framing és conservador i les stop rules es fan complir.
• És més barat del que esperava produir un preprint que sobrevisqui a una primera ronda de revisió per parells amb IA. El cost marginal del següent cas d’estudi, amb una quàdruple de llavors distinta, és petit.
• És un petit element d’evidència que la generació actual de models de llenguatge, usada amb cura i sota stop rules forçades, pot actuar com un assistent raonable de cerca creuada per a no-especialistes, sense sobre-reclamar i sense contaminar el graf de citacions.

Els riscos són reals i els nomeno explícitament a §6.2 del paper: blanqueig de reputació, contaminació del graf de citacions, càrrega asimètrica sobre els revisors humans. La defensa és estructural —les quatre stop rules i l’escala de confiança— i no afirmo que la defensa sigui suficient.

Per què poso el meu nom en això

No faria això si el pitjor cas fos “quedo en ridícul”. El pitjor cas per a mi és que un expert trobi un error embarassós i el preprint es corregeixi en v1.1. Això està bé. El pitjor cas per a la comunitat, si l’experiment és correcte en absolut, és que workflows com aquest comencin a produir preprints més ràpid del que els humans poden revisar-los. El paper de metodologia es pren aquest risc seriosament i l’aborda directament.

Prefereixo contribuir amb cura i arriscar-me que em diguin que estic passant per alt alguna cosa òbvia abans que no contribuir en absolut. El que tinc és energia i la paciència d’un enginyer de programari; el que proveeix l’experiment és una manera de convertir aquesta paciència en alguna cosa que un especialista pugui acceptar, refutar o contextualitzar ràpidament.

Què ve a continuació

El preprint del cas d’estudi —el paper acompanyant a aquest de metodologia— es dipositarà amb el seu propi DOI els pròxims dies, amb la invitació explícita als especialistes a enganxar-se amb ell. Després escriuré un post de seguiment aquí sobre el seu contingut en el mateix estil divulgatiu.

Després d’això, si la metodologia sobreviu al contacte expert, planejo provar un segon cas d’estudi amb una quàdruple de llavors deliberadament distinta, per veure si el workflow treu un tipus de descobriment distint o només la mateixa forma de resultat.

Si llegeixes algun dels dos preprints i tens un contraexemple, una referència coneguda, o un refinament, t’ho agrairia genuïnament. El punt sencer de les observacions conjecturals registrades és convidar a això.

El paper de metodologia és d’accés obert (CC-BY-4.0) sota el DOI 10.5281/zenodo.20184068. El repositori està a github.com/Dredok/axiom-explorer.