El problema de álgebra de bachillerato planteado por Alfred Tarski pregunta si toda identidad verdadera sobre la suma, la multiplicación y la exponenciación de enteros positivos se deduce a partir de una lista de once identidades elementales. El lógico Alex Wilkie demostró en los años setenta que existe una identidad válida sobre los enteros positivos que no se deduce de esos axiomas. A lo largo de las décadas, varios autores fueron reduciendo el tamaño mínimo de un contraejemplo —un álgebra finita que cumple los axiomas pero viola la identidad de Wilkie— hasta llegar a un contraejemplo de doce elementos debido a Stanley Burris y Marsha Yeats, mientras que Jian Zhang estableció que no podía existir un contraejemplo con menos de once elementos. Una nueva investigación, difundida como preprint en arXiv, resuelve definitivamente la cuestión: usando un solver de SAT, los autores demuestran que los contraejemplos más pequeños tienen efectivamente doce elementos, confirmando la conjetura de Burris y Yeats. El resultado va más allá: identifica exactamente 8.957.952 contraejemplos de doce elementos módulo isomorfismo y ofrece una clasificación sencilla de los mismos. El método basado en SAT supera en rendimiento a herramientas específicas para la búsqueda de contraejemplos en teorías ecuacionales, como Mace4 y SEM. Además, los autores recurren a la autoformalización para verificar la corrección del teorema principal en el asistente de demostración Lean, lo que aporta una garantía formal independiente. El trabajo ilustra el creciente peso de los métodos automatizados y de la verificación formal en la resolución de problemas abiertos de lógica algebraica.
Noticias agregadas con IA