Las máquinas contraatacan: la IA encuentra contraejemplos que desconciertan a los matemáticos
Human mathematicians are being outcounterexampled
En un periodo de dos meses, los sistemas de IA como ChatGPT, Sol y Fable han refutado conjeturas famosas, incluida la conjetura de la distancia unitaria de Erdős y una pregunta de Grothendieck sobre esquemas de grupo. Kevin Buzzard, matemático de Imperial College, relata cómo estos contraejemplos fueron verificados formalmente en Lean, y cómo la IA está acelerando la formalización de las matemáticas. También se discute el impacto en la comunidad matemática y la creciente aceptación de estas herramientas.
Me di cuenta de que ya no confiaba en muchos matemáticos humanos en lo que respecta a los detalles técnicos, descubrí Lean y empecé a argumentar que los demostradores interactivos de teoremas deberían desempeñar un papel importante en el futuro de las matemáticas.