Hoy, en su conferencia "The equational theories project", Terence Tao
defendió que la investigación matemática debe evolucionar hacia un
modelo colaborativo a gran escala, semejante al empleado en otras
disciplinas científicas. Esta transformación requiere el uso de
herramientas modernas como plataformas colaborativas (GitHub),
asistentes de prueba formales (Lean) y automatización mediante
inteligencia artificial. El proyecto ETP (Equational Theories Project)
constituye un ejemplo paradigmático de esta nueva aproximación a la
investigación matemática.
El proyecto nació de una pregunta aparentemente simple planteada en el
foro MathOverflow, pero pronto adquirió una dimensión extraordinaria:
mapear completamente el "gráfico de implicaciones" entre 4,692 leyes
algebraicas únicas dentro de estructuras elementales denominadas
magmas. Esta ambiciosa meta implicaba resolver más de 22 millones de
problemas individuales, donde cada par de leyes requería encontrar una
prueba de implicación o desarrollar un contraejemplo que la refutara. La
magnitud descomunal de este desafío lo convertía en una tarea imposible
de abordar mediante los métodos tradicionales de investigación
individual o de pequeños equipos.
La estrategia implementada por el ETP consistió en un flujo de trabajo
híbrido y descentralizado de notable innovación. La componente humana
aprovechó la creatividad de una extensa comunidad de colaboradores para
desarrollar pruebas y contraejemplos ingeniosos, mientras que la
componente computacional empleó masivamente probadores automáticos de
teoremas (ATPs) y otras herramientas para resolver millones de casos más
directos. El elemento fundamental que garantizó la integridad del
proyecto fue la formalización exhaustiva de cada resultado en el
asistente de pruebas Lean, asegurando una corrección absoluta y creando
una base de conocimiento completamente verificada y confiable.
En el plazo extraordinariamente breve de tres meses, el proyecto logró
resolver prácticamente la totalidad de los 22 millones de problemas
planteados. Además, el proceso de abordar los casos más complejos
estimuló el desarrollo de técnicas matemáticas innovadoras, culminando
con la formulación de un nuevo y fascinante problema abierto. El ETP
demostró que este modelo colaborativo trasciende la mera verificación de
conocimiento existente para convertirse en un motor poderoso de
descubrimiento matemático, estableciendo así un precedente exitoso para
una investigación matemática más abierta, transparente y asistida
computacionalmente.