OpenAI presume 722 resultados matemáticos, pero ya hay discrepancias en sus pruebas con Lean
Matemáticos consultados por The Verge y TechCrunch avisan de que verificar los 722 manuscritos llevará años, y ya han aparecido discrepancias entre pruebas en lenguaje natural y su formalización en Lean.