Ayer, en su conferencia "AI for Math: The future of collaborative discovery", Mateja Jamnik presentó una visión de la inteligencia artificial no como una simple herramienta para resolver problemas, sino como un socio colaborativo en el descubrimiento matemático. Su trabajo explora cómo las máquinas pueden proponer ideas y acelerar la investigación. A través de un estudio empírico con matemáticos, demostró que la interacción humano-IA es compleja; una respuesta de la IA no necesita ser perfectamente correcta para ser útil, ya que incluso ideas parcialmente erróneas pueden inspirar nuevas vías de pensamiento, mientras que respuestas correctas pero verbosas pueden resultar inútiles.

El núcleo técnico de su propuesta, materializado en trabajos como su artículo "Draft, sketch, and prove: Guiding formal theorem provers with informal proofs", es un ciclo auto-mejorable que integra el vasto conocimiento matemático informal. A través de la arquitectura ‘Borrador, Esquema y Prueba’ descrita en dicho artículo, la IA traduce pruebas humanas a un formato formal y riguroso. Este ciclo culmina en un sistema ‘conjeturador-demostrador’ que genera progresivamente nuevas conjeturas, las evalúa según su capacidad para ayudar a resolver problemas más difíciles y utiliza las mejores para mejorar continuamente, acercándose así a la resolución de teoremas que antes eran inaccesibles.

El objetivo final es integrar plenamente al ser humano en este ciclo de descubrimiento. Jamnik imagina un futuro donde los matemáticos interactúen con este sistema para proponer y evaluar conjeturas, guiando la dirección de la investigación. Su conclusión es que la IA no reemplazará a los matemáticos, sino que los potenciará, creando una sinergia entre la intuición humana y la capacidad de la máquina. El futuro de las matemáticas, según su visión, es una era de descubrimiento colaborativo entre humanos y máquinas.