Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

Magenta uses a training-free agentic pipeline to translate natural-language mathematical problems into Lean 4 statements for machine-checked verification. The system employs a statement judge to ensure formalization accuracy and an error-attribution judge to route failed proofs back to mathematical reasoning modules for iterative refinement.