En el artículo «Olympiad-level formal mathematical reasoning with reinforcement learning» se presenta AlphaProof, un agente de IA que utiliza aprendizaje por refuerzo para resolver problemas matemáticos complejos en el asistente de pruebas Lean. Combina una red neuronal con búsqueda en árbol para encontrar demostraciones formalmente verificables.

El sistema fue entrenado con millones de problemas auto-formalizados y emplea una innovadora adaptación en tiempo de prueba para los problemas más difíciles. Demostró capacidades excepcionales resolviendo problemas de competiciones como la Olimpiada Internacional de Matemáticas.

En la IMO 2024, AlphaProof resolvió tres problemas no geométricos, incluyendo el más difícil. Combinado con AlphaGeometry 2, el sistema logró una puntuación equivalente a medalla de plata, marcando un hito en el razonamiento matemático automatizado.