💻 computer science

SATisfying the High School Identities but not Wilkie's Identity

Este artículo resuelve una pregunta abierta en el problema del Álgebra de la Escuela Secundaria de Tarski al demostrar que ninguna álgebra de 11 elementos puede satisfacer las Identidades de la Escuela Secundaria mientras refuta la identidad de Wilkie, un resultado establecido mediante la codificación SAT y acompañado por el descubrimiento de un nuevo contramodelo de 12 elementos.

Autores originales: Agon Hajdari, Johannes Niederhauser

Publicado 2026-08-18

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Agon Hajdari, Johannes Niederhauser

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

En el vasto paisaje de las matemáticas, existe un rincón silencioso dedicado a las reglas que gobiernan cómo combinamos los números. Durante siglos, los matemáticos han dependido de un conjunto estándar de reglas para la suma, la multiplicación y la elevación de números a potencias —operaciones tan fundamentales que se enseñan en la escuela secundaria—. Estas reglas parecen absolutas, como las leyes de la física, porque funcionan perfectamente cuando contamos manzanas o calculamos distancias. Sin embargo, una pregunta profunda rondaba la mente de los lógicos: ¿son estas reglas familiares de la escuela secundaria suficientes para explicar cada verdad sobre estas operaciones? ¿Podría existir una regla oculta, verdadera para todos los números naturales, que no pueda derivarse de las fórmulas estándar de los libros de texto? Esta pregunta, conocida como el problema del álgebra de la escuela secundaria de Tarski, desafió la completitud de nuestro fundamento matemático. Si tal regla oculta existiera, significaría que nuestro conjunto estándar de axiomas era incompleto, dejando un vacío en nuestra comprensión de la aritmética.

Durante décadas, la respuesta permaneció elusiva. En la década de 1980, un matemático llamado Alex Wilkie descubrió una regla específica y compleja que es verdadera para los números naturales pero que no puede ser probada utilizando únicamente las identidades estándar de la escuela secundaria. Este fue un avance, pero dejó un nuevo rompecabezas: ¿qué tan pequeño puede ser un "contraejemplo"? Un contraejemplo en este contexto es un mundo matemático inventado donde las reglas estándar se mantienen verdaderas, pero la regla específica de Wilkie falla. Encontrar tal mundo demuestra que las reglas estándar no son suficientes. Los investigadores pasaron años buscando la versión más pequeña de este mundo. Para el año 2005, habían construido un contraejemplo con doce elementos distintos, y habían demostrado rigurosamente que no podía existir un contraejemplo con diez o menos elementos. Esto dejó un único y obstinado vacío: ¿podría existir un contraejemplo con exactamente once elementos?

Un equipo de investigadores de la Universidad de Innsbruck finalmente ha cerrado este vacío. Abordaron el problema no intentando construir el mundo matemático a mano, sino traduciendo toda la búsqueda en un enorme rompecabezas lógico que una computadora pudiera resolver. Tomaron los requisitos para un mundo matemático válido —donde la suma y la multiplicación se comporten normalmente— y la condición específica de que la regla de Wilkie debe fallar. Luego pidieron a una computadora que verificara cada forma posible de organizar un mundo de once elementos para ver si alguna de ellas satisfacía las condiciones. La computadora, utilizando técnicas avanzadas para descomponer el problema en miles de millones de diminutos pasos lógicos, encontró que no existe tal arreglo. La búsqueda fue exhaustiva y los resultados fueron verificados independientemente por diferentes herramientas de software para asegurar la certeza absoluta. La conclusión es definitiva: no existe un contraejemplo con once elementos. El contraejemplo más pequeño debe tener al menos doce elementos.

Los investigadores no se detuvieron en probar lo negativo. En el proceso de su búsqueda, también examinaron el caso de los doce elementos, que ya se sabía que era posible. Descubrieron un nuevo y distinto mundo de doce elementos que nunca antes había sido visto. Este nuevo mundo se comporta de manera diferente al encontrado en 2005, demostrando que hay más de una forma de romper las reglas del álgebra de la escuela secundaria manteniendo el resto del sistema intacto. Para alcanzar estas conclusiones, el equipo utilizó potentes recursos de computación paralela, ejecutando la búsqueda a través de docenas de procesadores simultáneamente. Generaron una prueba digital para sus resultados, un certificado que otros matemáticos pueden revisar para verificar que la computadora no cometió un error. Este proceso de verificación confirmó que la búsqueda de un contraejemplo de once elementos fue verdaderamente completa y que la respuesta es un "no" rotundo.

Este trabajo resuelve una pregunta abierta de larga data en el campo de la lógica ecuacional, confirmando que el número doce es el umbral crítico donde aparecen estas anomalías matemáticas. Demuestra que las identidades estándar de la escuela secundaria son suficientes para describir todas las verdades aritméticas para cualquier sistema de menos de doce elementos. El estudio también destaca el creciente poder de la computación moderna para resolver problemas teóricos profundos. Lo que antes era una tarea que requería años de esfuerzo manual e ingenio humano, se ha transformado en un proceso de verificación riguroso y automatizado. Los investigadores han proporcionado a la comunidad matemática un mapa completo del paisaje hasta el tamaño doce, mostrando exactamente dónde se mantienen las reglas conocidas y dónde finalmente se rompen. Sus hallazgos no son solo una lista de números, sino una línea de frontera definitiva en nuestra comprensión de la estructura aritmética, trazada con la precisión de una prueba verificada por computadora.

Resumen Técnico: Satisfaciendo las Identidades de la Escuela Secundaria pero no la Identidad de Wilkie

Planteamiento del Problema
El artículo aborda una instancia específica del problema de Álgebra de la Escuela Secundaria de Tarski, el cual pregunta si toda identidad que involucre suma, multiplicación y exponenciación que se cumple sobre los números naturales ( $\mathbb{N}$ ) es derivable de las Identidades de la Escuela Secundaria (HSI, por sus siglas en inglés). Wilkie demostró previamente que este no es el caso al exhibir una identidad que se cumple en $\mathbb{N}$ pero que no es derivable de las HSI. Para probar la no derivabilidad, se debe construir un modelo finito (un contramodelo) que satisfaga todos los axiomas de las HSI pero que falsifique la identidad de Wilkie.

Antes de este trabajo, la búsqueda del contramodelo más pequeño había reducido la brecha a un solo caso: mientras que se conocía un contramodelo de 12 elementos, búsquedas exhaustivas habían descartado tamaños hasta 10, dejando la existencia de un contramodelo de 11 elementos como la última cuestión abierta.

Metodología
Los autores formulan la búsqueda de contramodelos finitos como un problema de satisfacibilidad proposicional (SAT). Su enfoque involucra:

Restricciones Algebraicas y Poda: Los autores incorporan restricciones estructurales derivadas de la literatura algebraica previa (Burris, Lee, Zhang) para reducir el espacio de búsqueda. Estas incluyen:
- Fijar la cadena de "enteros" ( $1, 1+1, 1+1+1$ ) a elementos distintos $1, 2, 3$.
- Fijar el par testigo $(a, b)$ que falsifica la identidad de Wilkie a elementos no enteros específicos $4 $y$ 5$.
- Imponer condiciones de "colapso de enteros" (desigualdades) para evitar que el modelo degenere en una estructura donde la identidad de Wilkie se cumpliera accidentalmente.
- Imponer lemas de divisibilidad para asegurar que los términos específicos en la identidad de Wilkie no satisfagan relaciones que forzarían a la identidad a ser verdadera.
Codificación SAT: El problema se codifica en Forma Normal Conjuntiva (CNF).
- Variables: Las variables booleanas representan las tablas de operaciones para $+$ , $\times$ y $\exp$ sobre un dominio de tamaño $n$ . Variables adicionales rastrean la evaluación de términos compuestos dentro de la identidad de Wilkie.
- Cláusulas: La codificación impone que las operaciones sean funciones totales (exactamente una salida por cada par de entradas), satisfaga todos los axiomas de las HSI (asociatividad, conmutatividad, distributividad, leyes de exponenciación, leyes de identidad) y codifique explícitamente la negación de la identidad de Wilkie ( $LHS \neq RHS$ ).
- Complejidad: El número de variables crece como $\Theta(n^3)$ , mientras que el número de cláusulas crece como $\Theta(n^7)$ . Para $n=11$ , la instancia contiene aproximadamente 3,069 variables y 63.8 millones de cláusulas.
Resolución y Verificación: Los autores utilizan solvers SAT paralelos (Gimsatul y MallobSat) para resolver las instancias generadas. Crucialmente, emplean solvers que producen pruebas para generar certificados de insatisfacibilidad (formatos DRAT y LRUP). Estas pruebas son verificadas independientemente mediante verificadores formalmente verificados (GRAT y lrat_isa) para asegurar que los resultados sean matemáticamente rigurosos y estén libres de errores de implementación del solver.

Contribuciones Clave y Resultados

Resolución del Caso $n=11$ : El resultado principal es la prueba de que ningún álgebra de 11 elementos satisface los axiomas de las HSI refutando la identidad de Wilkie. Al demostrar que todas las instancias SAT para $n \le 11$ son insatisfacibles, los autores resuelven la última dimensión abierta por debajo de 12.
Verificación: Los resultados de insatisfacibilidad están respaldados por certificados verificados independientemente, proporcionando un alto grado de confianza en la conclusión.
Nuevo Contramodelo de 12 Elementos: Como subproducto de probar la codificación para $n=12$ , los autores descubrieron un contramodelo de 12 elementos que no es isomorfo al ejemplo de 12 elementos previamente conocido. También identificaron que existen más de 500 álgebras de Gurevič–Burris (GBAs) de 12 elementos no isomórficas, aunque una enumeración completa no era factible dentro de su tiempo disponible.
Análisis de Rendimiento: El estudio demuestra que los solvers SAT paralelos modernos son capaces de manejar la alta complejidad ecuacional de este problema, una tarea que anteriormente se consideraba demasiado difícil para los enfoques basados en SAT (como señaló el trabajo de Zhang en 2005). MallobSat resultó significativamente más rápido que Gimsatul y la línea base de un solo hilo (CaDiCaL) para instancias más grandes ( $n \ge 10$ ).

Significancia
El artículo afirma resolver el último tamaño abierto para la búsqueda de contramodelos finitos de la identidad de Wilkie, confirmando que 12 es el tamaño mínimo en el que tales contramodelos pueden ocurrir. El trabajo sirve como una demostración del progreso en el razonamiento automatizado, mostrando que los solvers SAT modernos pueden abordar eficazmente problemas de lógica ecuacional complejos que anteriormente eran intratables para estas herramientas. Los autores enfatizan que su contribución es la resolución definitiva del caso $n=11$ a través de la resolución SAT verificada por máquina, en lugar del descubrimiento de nueva teoría algebraica o aplicaciones más allá del alcance del problema de Tarski.

Más como este