OpenAI ha subido a GitHub el mayor repositorio de demostraciones matemáticas generadas por inteligencia artificial jamás publicado: 722 manuscritos agrupados en 372 familias de teoremas, todos verificados formalmente con Lean, el asistente de pruebas que la comunidad matemática usa para confirmar que un argumento no tiene fisuras lógicas. El repositorio está disponible en github.com/openai/math desde el 7 de octubre de 2026 y fue producido con el mismo modelo que en julio resolvió un problema abierto de las ecuaciones de Navier-Stokes. Continúa leyendo «OpenAI publica 722 demostraciones matemáticas generadas por IA: el mayor corpus verificado de la historia»