Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.
Alex: Welcome to another episode of ResearchPod. Today we're looking at a paper about turning ordinary written math into a form that a computer can actually verify — and how to do that more reliably than anyone has managed before.
Sam: When you say "verify," what does that mean exactly?
Alex: So imagine you write down a math statement in plain English — something like "every even number greater than two is the sum of two primes." A computer can't check that on its own. But if you rewrite it in a very precise programming language called Lean 4, the computer can check whether your statement is logically consistent and well-formed. That process — going from informal math to verified Lean code — is called formalization.
Sam: And the hard part is getting the translation right?
Alex: Right. And it's harder than it sounds. Lean 4 uses a massive library of pre-built mathematical definitions called Mathlib. Think of it like a giant, very precise dictionary where every word has an exact legal meaning. If your translation uses the wrong definition — even slightly — the statement can look fine on the surface but quietly mean something different underneath.
Sam: So you could write something that passes the computer's grammar check but still gets the math wrong?
Alex: Exactly. That's the core problem the paper is trying to solve. The system they build doesn't just translate once and hope for the best. It works in a loop. First, before writing any Lean code, the system searches Mathlib for relevant definitions and existing formalizations. Think of it like checking your class notes before rewriting a problem in a stricter format — you want to use the same vocabulary the library already uses.
Sam: And if the first attempt still goes wrong?
Alex: Then two separate checkers step in. One asks: can Lean actually compile this code? The other asks: does this formal statement still mean the same thing as the original sentence? If either check fails, the system revises the draft rather than discarding it entirely.
Sam: So the correction loop is built into the method, not bolted on afterward.
Alex: That's the key insight. The paper's argument is that formalization should be a back-and-forth process, not a single guess. And the paper includes a concrete case study that shows why this matters. In one example, the first translation compiled successfully — the grammar was fine — but it had quietly made a condition stricter than the original. The semantic checker caught that the meaning had shifted, a second retrieval step pulled in the missing library detail, and the revised version was correct.
Sam: So retrieval isn't just background context. It can actively fix a mistake that compilation alone would never catch.
Alex: Exactly. And that distinction — between "does it compile" and "does it mean the right thing" — is what makes the two checkers doing different jobs so useful. They catch different kinds of errors.
Sam: Where does the training data come into this?
Alex: So using this pipeline, the authors build a large dataset of verified Lean 4 examples — examples that have already survived both kinds of checking. They call it FormalVerse. That dataset is then used to train a model called MathForm-8B. The idea is that the model learns from outputs the pipeline itself can trust, rather than from raw guesses.
Sam: So the pipeline produces good examples, and those examples teach the model to do better on its own.
Alex: That's the idea. The paper describes it as a kind of co-evolution: the pipeline generates checked examples, and those examples help train a stronger model that can eventually handle more in a single pass. You're trying to compress a careful multi-step process into something the model internalizes.
Sam: Did that actually help on harder problems?
Alex: The evidence points that way. On the more difficult benchmarks — particularly in algebra, where Lean's type structure and existing library formalizations matter most — the full method outperformed simpler approaches. Human reviewers also confirmed the same overall ranking, which matters because it suggests the improvement wasn't just an artifact of one automatic checker being easy to fool.
Sam: What are the limits? Where does this still struggle?
Alex: The sober takeaway is that the approach depends heavily on good retrieval and good checking. If the library search misses the right concept, or if the original statement is genuinely ambiguous, the pipeline can still produce an incorrect formalization. It's not a solution to every problem — it's a meaningful reduction in avoidable mistakes.
Sam: So it's less about replacing human judgment and more about building a system that fails less often on the kinds of errors that are preventable.
Alex: That's a fair summary. The contribution is a careful way to connect informal mathematics, library knowledge, and verified Lean output — and to use that connection both to build better training data and to train a stronger model. It's a practical step forward, and an honest one about where the limits still are. Thanks for listening to ResearchPod.