Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
This paper introduces Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and constructs a machine-checked proof, which achieves 100% accuracy across all evaluated olympiad benchmarks.
Joshua Ong Jun Leang, Hao-Nan Li, Zheng-Yang Zhao et al.
· 0 citations