El artículo «What happens when AI starts checking mathematicians’ work» comenta que la comunidad matemática cuenta ahora con una herramienta de IA desarrollada por Math, Inc. llamada Gauss. Este sistema traduce demostraciones matemáticas al lenguaje formal de Lean y verifica su corrección, lo que agiliza la revisión de trabajos y garantiza la validez de los resultados.

Un equipo de investigadores liderado por Hariharan inició la formalización de las demostraciones de Maryna Viazovska sobre el empaquetamiento de esferas en dimensiones superiores. Sin embargo, Math, Inc. completó la formalización de forma autónoma utilizando Gauss, lo que suscitó interrogantes sobre la colaboración y el impacto de la IA en la investigación.

La formalización exitosa de las demostraciones de Viazovska marca un hito importante. Aunque la tecnología tiene limitaciones, su potencial para detectar errores, mejorar la precisión y fomentar nuevos descubrimientos es prometedor. El futuro de las matemáticas podría depender de la colaboración entre humanos y la IA.