Antonio Casares Santos

Los problemas que aborda Antonio Casares Santos en su investigación tienen su origen en la búsqueda de algoritmos para la demostración automática de teoremas matemáticos expresados mediante fórmulas en distintos tipos de lógicas. «En algunos casos —explica—, un intento de demostración puede abstraerse como un juego entre dos jugadores antagonistas. Un método para la obtención de algoritmos de demostración automática consiste en demostrar que, en estos juegos, basta utilizar estrategias simples dadas por una lista de instrucciones sencillas». Precisamente, uno de los temas centrales de su trabajo es el estudio de la complejidad de estrategias necesarias para ganar en distintos tipos de juegos combinatorios.

Tras graduarse en Matemáticas por la Universidad de Valladolid en 2019 y obtener el máster en Lógica Matemática en la Universidad de París Cité en 2020, Casares se doctoró en 2023 por la Universidad de Burdeos. Posteriormente fue investigador posdoctoral tanto en la Universidad de Varsovia (Polonia) como en la Universidad de Kaiserslautern- Landau (Alemania), y actualmente es profesor asociado de Informática Teórica en la Universidad de Aix-Marsella (Francia).

Su trabajo explora los límites de la computación, analizando qué problemas pueden resolverse mecánicamente a través de algoritmos. En particular, investiga desde el ámbito de la lógica la creación de algoritmos capaces de determinar la veracidad o falsedad de enunciados matemáticos, lo cual posee aplicaciones directas en la verificación formal de sistemas informáticos. «La lógica no sirve únicamente para escribir teoremas matemáticos. Estos formalismos lógicos se usan hoy en día para describir las especificaciones de programas informáticos. En este contexto, los métodos que estudio permiten verificar automáticamente que un programa informático funciona correctamente».

Fascinado por las matemáticas desde niño tras recibir un libro de acertijos como regalo, decidió dedicarse a esta disciplina atraído por la precisión del lenguaje matemático y la robustez de su conocimiento: «En matemáticas, toda demostración tiene que ser convincente, lo que nos lleva a preguntarnos qué quiere decir que un argumento sea convincente o qué podemos establecer como una verdad básica». Estas reflexiones, que se adentran en el terreno de la filosofía, despertaron su interés por la lógica y le impulsaron a orientar su trabajo hacia desafíos contemporáneos, acelerados por el auge de la inteligencia artificial: «Desde hace unos años, nos enfrentamos a grandes retos tanto tecnológicos como también sociales y ambientales, y creo que las matemáticas, precisamente por su precisión y robustez, pueden ofrecer muchas herramientas para analizarlos y hacerlos avanzar».