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.