En su conferencia "Will computers prove theorems?", Kevin Buzzard plantea que los ordenadores ya demuestran teoremas, pero la pregunta crucial es cómo pueden transformar la investigación matemática. Aunque reconoce la utilidad de las herramientas actuales como las redes neuronales para identificar patrones, su aplicación permanece limitada. Los modelos de lenguaje como ChatGPT, por su parte, pueden ofrecer ideas valiosas, pero fracasan rotundamente en el razonamiento lógico: tienden a "alucinar" o inventar detalles para parecer convincentes, lo que los convierte en herramientas poco confiables para las matemáticas rigurosas.

La solución que propone Buzzard para superar estas limitaciones radica en la sinergia entre la inteligencia artificial y los asistentes de demostración formal como Lean. Su propuesta consiste en entrenar modelos de IA para que generen pruebas directamente en código de Lean, en lugar de utilizar lenguaje natural. De este modo, el asistente de demostración funciona como un verificador infalible: cualquier argumento lógicamente incorrecto será rechazado automáticamente por el sistema. Esta metodología obligaría a la IA a evolucionar desde la mera imitación de patrones hacia la construcción de razonamientos lógicamente verificables.

No obstante, el principal obstáculo para materializar esta visión es la escasez de matemáticas modernas y avanzadas formalizadas en Lean, elementos esenciales para el entrenamiento de estos modelos. Buzzard concluye con un llamamiento directo a la comunidad matemática: considera que es responsabilidad de los investigadores emprender la tarea fundamental de formalizar el conocimiento de sus respectivos campos, tal como él mismo está haciendo con el último teorema de Fermat. Argumenta que este esfuerzo resulta crucial para desarrollar las herramientas que revolucionarán la disciplina, a pesar de que el sistema académico actual no reconozca ni recompense adecuadamente este tipo de contribuciones.