Sage: Formalization with Semantic Correction

Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni +3

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 pr…