Sage: Formalization with Semantic Correction.

arXiv:2609.35790v2 Announce Type: replace-cross Abstract: While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 formal statements are already provided. Translating in