axiom-explorer: un experimento honesto en descubrimiento matemático asistido por LLM

El primer preprint de un pequeño experimento mío ya está en Zenodo. El preprint describe una herramienta que construí —no un teorema que demostré— y el workflow que implementa. Quiero contarte de qué va sin la retórica habitual sobre la inteligencia artificial resolviendo las matemáticas, porque el experimento es más modesto que eso y su honestidad es precisamente la parte que creo que vale la pena compartir.

La pregunta

Hay una tensión persistente en matemáticas entre la velocidad a la que se producen ideas fundacionales nuevas y la velocidad a la que la comunidad puede explorar sus consecuencias en otras ramas. Cuando aparece un marco axiomático fresco —la matemática condensed en 2019, el programa de la dualidad sintética de Stone en 2024— pasan años hasta que la polinización cruzada con otras ramas cristaliza en resultados citables. La mayor parte de ese tiempo no se va en pruebas difíciles, sino en el trabajo más sencillo de descubrir dónde dos comunidades están hablando calladamente de lo mismo en vocabularios distintos.

La pregunta es si un workflow cuidadoso y bien acotado puede hacer parte de ese trabajo de descubrir-dónde y presentar los resultados como invitaciones falsables a revisión experta.

El instrumento

axiom-explorer es ese instrumento. Es un harness en Python con un puñado de herramientas externas (arXiv, Mathlib4, Z3, SymPy, Lean 4, latexmk) y un modelo de lenguaje grande como orquestador. El orquestador es la parte que más probablemente pone nerviosa a la gente —razonablemente— y el diseño de la herramienta consiste en gran medida en restringir qué puede hacer el orquestador.

El workflow corre en cinco fases:

1. Mapeo bibliométrico. El harness elige un conjunto pequeño de “semillas axiomáticas modernas y productivas” de ramas distintas —en esta corrida: el axioma de univalencia de la teoría de tipos homotópica, la matemática condensed, los espacios perfectoides, y la curvatura de Ricci sintética— y consulta arXiv en sus combinaciones por pares usando cinco estrategias de búsqueda distintas. La salida es una puntuación de densidad por par.
2. Inventario del estado formal. Para cada semilla, el harness escanea la biblioteca Mathlib4 y proyectos adyacentes en Lean y Agda, contando archivos, definiciones, y TODOs explícitos.
3. Dossieres por par. Para los pares que sobreviven a la Fase 0, construye un dossier integrando literatura, funtores puente, y experimentos numéricos o simbólicos a pequeña escala.
4. Inmersión profunda. Los candidatos que sobreviven a los dossieres se promueven a su propio dossier con enunciado preciso, evidencia, y un nivel de confianza explícito en una escala de cuatro niveles.
5. Síntesis y reporte. Los candidatos supervivientes y el meta-análisis metodológico se convierten en un borrador de preprint que después se itera contra varias rondas de revisión por pares mediante IA antes de que se acerque a cualquier revisor humano.

La escalera de confianza

Cada afirmación que el harness saca a la superficie lleva una etiqueta:

• L0 — verificado mecánicamente. Z3 no encontró contraejemplo. Lean type-chequea los axiomas.
• L1 — fuerte. Un resultado estándar y citado, con referencia.
• L2 — plausible. Argumentado por el workflow, no verificado directamente.
• L3 — especulativo. Una conjetura que emerge de la búsqueda cruzada, registrada como pregunta, nunca como afirmación.

Este es el dispositivo de protección descendente más importante. Es la diferencia entre un preprint que promete certeza al estilo folklore y uno que entrega al lector exactamente el nivel de confianza que el workflow se ha ganado.

Las stop rules

El orquestador tiene cuatro stop rules duras que el workflow se niega a saltar:

• No publica en Zenodo ni en ningún otro sitio sin que el autor humano pulse explícitamente el botón de publicar.
• No envía emails ni ninguna otra comunicación externa; los borradores se producen, el autor humano los despacha.
• No reclama novedad más allá de una forma muy estrecha: “esta formulación no aparece como tal en ninguna fuente única que hayamos encontrado”.
• No suplanta autoridad matemática. La identidad del autor y el método de producción asistido por LLM se declaran en la portada de cada preprint que sale.

Estas se comprueban en los puntos de revisión de código. El harness se niega a marcar un candidato como “listo” hasta que la escalera de confianza está rellenada y la disclosure está en su sitio.

El bucle de revisión por pares con IA

Esta es la parte que más me sorprendió durante el experimento. El borrador de la Fase 5 se somete a varios revisores LLM distintos (familias de modelo distintas, prompts distintos) antes de cualquier revisión humana. Cada ronda produce una crítica estructurada que el orquestador tiene que abordar punto por punto, con retracción explícita de cualquier afirmación anterior que la revisión haya demostrado equivocada.

En el caso de estudio que ejecutamos, cuatro rondas de revisión por pares con IA (v1→v1.1, v1.1→v1.2, v1.2→v1.2.1, v1.2.1→v1.2.2) atraparon tres errores matemáticos sustantivos que el borrador original contenía:

• Un fallo de invariancia en un invariante de tamaño clave.
• Una cota de cardinalidad sobre grupos profinitos libres expresada en una forma inconsistente con las atestaciones geométricas que se citaban.
• Un ejemplo modelo-teórico que yo había clasificado como trivial cuando en realidad es el grupo de Galois absoluto de los racionales.

Una quinta ronda atrapó un error de cita (un identificador de arXiv que apuntaba a un paper sobre turbulencia en vez del trabajo previsto sobre grupos de Lascar). Ninguno de ellos habría sido cazado por una sola generación LLM. Todos ellos fueron cazados antes de que se acercara ningún revisor humano experto.

El bucle no sustituye a la revisión experta. Es, sin embargo, una primera línea de defensa notablemente barata y eficaz.

El caso de estudio, brevemente

Corrí el workflow sobre una cuádrupla de semillas. Lo que salió es el tema de un segundo preprint aparte —el paper conjetural acompañante, forthcoming— que depositaré con su propio DOI en los próximos días. El resumen corto es que el harness me dirigió a dos papers recientes y llamativos que no había leído con cuidado (el trabajo de Haine et al. sobre el tipo de homotopía condensed de un esquema, y el propio paper de Haine de 2026 que unifica el grupo fundamental proétale de un esquema con el grupo de Lascar de una teoría completa de primer orden), y leer los dos a la vez sugería una envolvente cardinal candidata que, hasta donde pude comprobar, no aparece escrita en ninguna fuente única.

Ese candidato se presenta como una conjetura falsable, con etiquetas de confianza explícitas, y el preprint acompañante es una invitación abierta a especialistas en matemática condensed, teoría de modelos y teoría de conjuntos a hacer exactamente lo que los especialistas hacen: confirmarlo como folklore, encontrar un contraejemplo, o refinarlo. Cualquiera de los tres es un excelente resultado.

Lo que creo que vale el experimento

No soy un matemático con doctorado. Trabajo en la frontera entre la ingeniería de software y los métodos formales, y no tengo nada que hacer escribiendo sobre $\infty$-topoi sin ayuda explícita. Lo primero que hace el workflow es dejar eso obvio en cada artefacto que produce.

Lo que sí creo que vale el experimento, en su alcance correcto, es:

• Es honestamente publicable como una observación registrada, con un DOI, precisamente porque el framing es conservador y las stop rules se hacen cumplir.
• Es más barato de lo que esperaba producir un preprint que sobreviva a una primera ronda de revisión por pares con IA. El coste marginal del siguiente caso de estudio, con una cuádrupla de semillas distinta, es pequeño.
• Es un pequeño elemento de evidencia de que la generación actual de modelos de lenguaje, usada con cuidado y bajo stop rules forzadas, puede actuar como un asistente razonable de búsqueda cruzada para no-especialistas, sin sobre-reclamar y sin contaminar el grafo de citas.

Los riesgos son reales y los nombro explícitamente en §6.2 del paper: blanqueo de reputación, contaminación del grafo de citas, carga asimétrica sobre los revisores humanos. La defensa es estructural —las cuatro stop rules y la escalera de confianza— y no afirmo que la defensa sea suficiente.

Por qué pongo mi nombre en esto

No haría esto si el peor caso fuera “quedo en ridículo”. El peor caso para mí es que un experto encuentre un error embarazoso y el preprint se corrija en v1.1. Eso está bien. El peor caso para la comunidad, si el experimento es correcto en absoluto, es que workflows como este empiecen a producir preprints más rápido de lo que los humanos pueden revisarlos. El paper de metodología se toma ese riesgo en serio y lo aborda directamente.

Prefiero contribuir con cuidado y arriesgarme a que me digan que estoy pasando por alto algo obvio antes que no contribuir en absoluto. Lo que tengo es energía y la paciencia de un ingeniero de software; lo que provee el experimento es una manera de convertir esa paciencia en algo que un especialista pueda aceptar, refutar o contextualizar rápidamente.

Qué viene a continuación

El preprint del caso de estudio —el paper acompañante a este de metodología— se depositará con su propio DOI en los próximos días, con la invitación explícita a los especialistas a engancharse con él. Luego escribiré un post de seguimiento aquí sobre su contenido en el mismo estilo divulgativo.

Después de eso, si la metodología sobrevive al contacto experto, planeo probar un segundo caso de estudio con una cuádrupla de semillas deliberadamente distinta, para ver si el workflow saca un tipo de hallazgo distinto o solo la misma forma de resultado.

Si lees alguno de los dos preprints y tienes un contraejemplo, una referencia conocida, o un refinamiento, te lo agradecería genuinamente. El punto entero de las observaciones conjeturales registradas es invitar a eso.

El paper de metodología es de acceso abierto (CC-BY-4.0) bajo el DOI 10.5281/zenodo.20184068. El repositorio está en github.com/Dredok/axiom-explorer.