Demostración matemática por inteligencia artificial a nivel de Olimpiada (AlphaProof, FunSearch)
AI mathematical proving at Olympiad level
- Fecha
- 2024-2025 · fiabilidad alta
- Lugar
- Londres (Google DeepMind), Reino Unido
- Autoría
- Google DeepMind (AlphaProof y AlphaGeometry 2, 2024; FunSearch, 2023); sistemas de OpenAI y DeepMind con nivel de medalla de oro en la IMO de 2025
- Ámbito
- Saber y símbolos
⚠️ Dato en discusión: las fuentes no coinciden.
Qué se descubrió
Sistemas de IA que resuelven problemas de la Olimpiada Internacional de Matemáticas con pruebas verificadas en Lean (plata en 2024, oro en 2025) y que descubren construcciones nuevas, como una mejor cota inferior en el problema del cap set (FunSearch). Inicio del descubrimiento matemático asistido por IA.
Se debate cuánto del mérito matemático corresponde a los sistemas; los resultados de 2025 son recientes y su alcance en investigación real aún se evalúa.
A qué dio paso
- colaboración humano-IA en investigación matemática
- formalización automática
- nuevos resultados combinatorios
Se apoya en
- Formalización en Lean: Liquid Tensor Experiment y mathlib2022
- Lean y mathlib
- AlphaGo y aprendizaje por refuerzo
- demostración automática de teoremas
Hizo posible
- asistentes de investigación matemática