Este trabajo muestra que Lean puede servir como un oráculo simbólico de proceso, proporcionando retroalimentación fina y verificada durante el aprendizaje por refuerzo. Al analizar los intentos de demostración en secuencias de tácticas y usar la elaboración de Lean para marcar pasos válidos y primeros fallos, el sistema genera señales de recompensa densas basadas en teoría de tipos. Los experimentos demuestran que la supervisión a nivel de táctica supera a los métodos solo de resultado en benchmarks como MiniF2F y ProofNet, destacando el papel de Lean tanto como evaluador como fuente de recompensa de entrenamiento.