Sage-to-Lean: Formal Verification of Answers from CAS-Augmented Mathematical Agents

Language models equipped with computer algebra systems can perform numerical and symbolic experiments, search for hypotheses, and solve research-level mathematical problems. However, apart from it, the verification of the generated results remains a challenging task, often requiring heuristic graders or human intervention. We propose Sage-to-Lean, a framework in which a Lean~4 agent receives the problem, a SageMath agent's answer, its informal derivation, and must produce a formal proof or refutation. These two stages form a partial workflow for automated discovery: SageMath supported hypothesis generation, then Lean-checked certification. On 50 research-level arXiv problems the verifier reached a verdict on 10, all replaying in Mathlib. We analyze the outcome structure and show how accepted certificates and stalled traces alike can route the next revision in a closed discovery loop. The code is available in the public repository https://github.com/Germandev55/sage-to-lean.