El artículo «Solving formal math problems by decomposition and iterative reflection» presenta Delta Prover, un nuevo sistema que resuelve problemas matemáticos complejos. Este agente utiliza un LLM que interactúa con el asistente de pruebas Lean 4. Mediante una descomposición de problemas y una reparación iterativa de las pruebas, el sistema aprende de los errores para construir demostraciones verificables. Alcanza un rendimiento del 95.9% de éxito en los problemas de miniF2F, superando a otros métodos sin necesitar un costoso reentrenamiento del modelo.