Equational Theories Project: 22 millones de implicaciones

Hay una operación de la que no se sabe nada: no es la suma ni el producto, no es conmutativa, no es asociativa, no tiene elemento neutro. Es solo una regla que toma dos cosas de un conjunto y devuelve otra. Los matemáticos la llaman magma, y es lo más desnudo que existe en álgebra: un conjunto y una operación binaria, sin más axiomas. En septiembre de 2024, Terence Tao propuso un juego con esa nada: tomar las 4694 leyes más sencillas que un magma puede cumplir y averiguar, para cada pareja de leyes, si una obliga a la otra. Quince meses después, el informe final decía que el mapa estaba completo. O casi.

Un conjunto, una operación y muchas leyes

Escribamos la operación como $x \circ y$. Una ley es una igualdad que se pretende cierta para todos los valores de las variables. La conmutativa, $x \circ y = y \circ x$, es una ley. También lo es la asociativa, $x \circ (y \circ z) = (x \circ y) \circ z$, y la idempotente, $x \circ x = x$. Y hay leyes más exóticas, como $x = y$, que solo se cumple en un magma con un único elemento.

El proyecto se limitó a las leyes en las que la operación aparece como mucho cuatro veces. Contarlas es un problema de combinatoria con trampa: hay que descontar las que son idénticas salvo cambiar el nombre de las variables o darle la vuelta a la igualdad. Tao hizo una estimación inicial de 4665, y un comentarista de su blog, Amir Livne Bar-on, las enumeró de verdad y le salieron 4694. Esa es la cifra buena, y el comentarista terminó figurando entre los autores del informe final.

La pregunta del proyecto es una implicación entre leyes. Decimos que la ley A implica la ley B si todo magma que cumple A cumple también B. Con 4694 leyes hay $4694 \times 4693 = 22\,028\,942$ parejas ordenadas de leyes distintas, y si se cuenta también cada ley consigo misma son $4694^2 = 22\,033\,636$ casos. Unos veintidós millones de preguntas de sí o no.

Cómo se responde a una pregunta

Hay dos maneras de cerrar una implicación, y son muy distintas.

Para decir que sí, hay que demostrar. Un ejemplo pequeño: supón que una operación es a la vez asociativa y conmutativa. ¿Cumple entonces $x \circ (y \circ z) = y \circ (x \circ z)$? Sí:

$$x \circ (y \circ z) = (x \circ y) \circ z = (y \circ x) \circ z = y \circ (x \circ z).$$

La primera igualdad usa la asociativa, la segunda la conmutativa en $x \circ y$ y la tercera la asociativa otra vez. Esa cadena de reescrituras es una demostración completa, y es exactamente el tipo de cosa que un programa puede buscar por fuerza bruta inteligente.

Para decir que no, basta un magma que cumpla A y rompa B. La figura muestra uno con tres elementos, definido por $x \circ y = -(x+y)$ módulo 3. Su tabla es simétrica, así que es conmutativo, pero $(1\circ 0)\circ 0 = 1$ mientras que $1\circ(0\circ 0) = 2$. La conmutativa, por tanto, no implica la asociativa.

Conviene notar la asimetría. Demostrar exige un argumento que valga para todos los magmas del universo. Refutar exige encontrar un solo ejemplo, pero encontrarlo puede ser endiabladamente difícil, porque los magmas son una selva: solo con cuatro elementos hay $4^{16} = 4\,294\,967\,296$ tablas de operación posibles.

Una colaboración abierta

El proyecto se lanzó el 25 de septiembre de 2024 con una entrada en el blog de Tao, planteado como un experimento sobre cómo colaborar en matemáticas con ayuda de máquinas. La pregunta original venía de una consulta en MathOverflow de julio de 2023. Los mantenedores fueron tres: el propio Tao, Pietro Monticone y Shreyas Srinivas. A su alrededor se juntaron más de cincuenta personas, que se coordinaban en un repositorio de GitHub, en un canal de Zulip y con visualizadores para explorar las leyes y los magmas. El informe final lo firman 34 autores en arXiv, pero quienes contribuyeron fueron más.

El ritmo fue vertiginoso. Menos de tres semanas después, el 12 de octubre de 2024, el propio Tao daba el proyecto por completado en un 99,9963 %. El propio Tao cuenta que se tardó unos dos meses en resolver informalmente casi todo y unos cinco más en formalizarlo en Lean. El objetivo principal, tener decidida cada implicación y verificada, se dio por alcanzado el 14 de abril de 2025.

Lo que decidieron los números

El resultado es una fotografía exacta de ese universo de leyes. De los 22 033 636 casos posibles (incluida la implicación trivial de cada ley consigo misma), 8 178 279 (el 37,12 %) son verdaderos y 13 855 357 (el 62,88 %) falsos. Las leyes se agrupan en 1415 clases de equivalencia, es decir, grupos de leyes que se implican entre sí. La clase más grande tiene 1496 leyes, todas equivalentes a $x = y$: son distintas por fuera, pero obligan al magma a tener un único elemento.

Aquí hay un matiz que se pierde en los titulares. Los 22 millones son parejas posibles, no teoremas distintos que alguien escribiera uno a uno. Solo 10 657 implicaciones positivas y 586 925 negativas hubo que formalizar directamente en Lean. El resto salió de dos principios sencillos. El primero es la transitividad: si A implica B y B implica C, entonces A implica C, y nadie tiene que probarlo. El segundo es la dualidad: si en una ley se intercambia el orden de los dos argumentos de cada producto, se obtiene otra ley, y todo lo que se pruebe para una vale, espejado, para la otra.

Máquinas, pero cuáles

Conviene precisar qué máquinas se usaron. El proyecto no lo resolvió una inteligencia artificial moderna. Lo dice el propio Tao: las herramientas actuales de IA no jugaron un papel importante, porque los demostradores automáticos clásicos eran más baratos y resolvían casi todo lo que la IA podía resolver. Los demostradores más usados fueron Vampire y Prover9/Mace4, con apoyo puntual de otras herramientas como Z3, Duper o egg. Algunos participantes usaron GitHub Copilot para acelerar la escritura de pruebas en Lean y de otro código, y varios visualizadores se escribieron con ayuda de modelos de lenguaje, pero eso es otra cosa.

Los refutadores trabajaron por fuerza bruta. Una búsqueda exhaustiva en todos los magmas de hasta cuatro elementos (unos 4300 millones), de 165 horas de CPU, refutó 13 632 566 implicaciones, la gran mayoría de los casi 13,9 millones de falsas; para todas ellas bastaron 524 magmas distintos. Luego vino lo difícil. Cuando Tao hizo su balance de octubre de 2024 quedaban menos de mil implicaciones abiertas, y según el informe final unas dos docenas de resultados negativos exigieron construcciones delicadas hechas a medida. La más dura, que E1729 no implica E817, costó meses de trabajo y unas 4000 líneas de Lean.

Lean fue el notario. Los demostradores automáticos pueden equivocarse o ser oscuros, así que sus pruebas no se aceptaron por la cara: se reconstruyeron en Lean, que comprueba cada paso, usando certificados en lugar de fiarse de la salida del programa. Así, un resultado del proyecto no es “Vampire dice que sí”, sino “Lean lo ha comprobado”.

Lo que sigue abierto

Quedó una pregunta sin cerrar, y es hermosa. En magmas finitos, todo está resuelto salvo una implicación y su dual: si la ley E677 implica la ley E255. Para magmas arbitrarios se sabe que no, pues existe un contraejemplo, que además es infinito. Los autores sospechan, de forma tentativa, que tampoco lo implica en el caso finito, pero nadie ha encontrado un magma finito que cumpla E677 y no E255. Según la información pública que he podido consultar, a 15 de octubre de 2026 sigue abierta. El 10 de octubre un colaborador abrió una propuesta en GitHub con un resultado condicional en Lean, todavía sin revisar, y aclaró que no resuelve el caso general.

El mapa, entretanto, sigue dando frutos. En marzo de 2026 Tao y Damek Davis lanzaron, con la SAIR Foundation, un desafío para que modelos baratos respondieran preguntas del conjunto de datos del proyecto con ayuda de una hoja de ayuda de no más de 10 KB. Según el anuncio de la primera etapa, sin hoja acertaban alrededor del 50 % y con ella entre el 55 y el 60 %; el desafío preveía además una segunda etapa, de cuyos resultados no tengo una fuente primaria. Y en enero de 2026, Berlioz y Melliès construyeron un espacio latente de teorías ecuacionales a partir de estos datos.

Queda la lección del conjunto. Un territorio entero de álgebra, 22 millones de preguntas, se cartografió en meses porque se repartió bien, se dejó que cada uno aportara lo que sabía, se verificó con una máquina implacable y se aceptó dejar un último rincón en blanco. A veces la matemática más honesta es la que termina con un mapa y una pregunta abierta.

Practica: cuenta cuántas tablas de operación admite un conjunto.

Fuentes

• Bolan, M., Tao, T. et al. (2025). The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. arXiv:2512.07087.
• Equational Theories Project (web del proyecto). teorth.github.io.
• Tao, T. (2024). A pilot project in universal algebra to explore new ways to collaborate and use machine assistance? What’s new (blog).
• Tao, T. (2024). The Equational Theories Project: a brief tour. What’s new (blog).
• Tao, T. (2025). The Equational Theories Project: advancing collaborative mathematical research at scale. What’s new (blog).
• Tao, T. (2026). Mathematics Distillation Challenge: Equational Theories. What’s new (blog).
• Berlioz, L., Melliès, P.-A. (2026). The Latent Space of Equational Theories. arXiv:2601.20759.
• Issue #1517 del repositorio equational_theories. GitHub, 2026.