🧮 Introducing MathForm, an open-source framework, dataset, and model for mathematical autoformalization with Lean 4.

Formalizing mathematics makes mathematical knowledge machine-checkable, but it is more than translating statements into code. A model must map each concept onto the right types and definitions in Mathlib. A formal statement can compile and still misstate the original problem.

Highlights ✨
MathForm Framework: Retrieval-Augmented, Verification-Guided Data Construction A retrieval planner pulls the Mathlib definitions and existing formalizations a statement needs. The generator then revises its output against Lean compiler diagnostics and semantic-consistency feedback for up to 3 rounds.

FormalVerse Dataset: 367K+ Verified Lean 4 Examples Each example pairs a natural-language statement with verified Lean 4 code , across diverse mathematical domains and sources.

Results 📊
• At a matched 100K budget with the same recipe and init, models trained on FormalVerse reach 60.32% Consistency Check, vs 46.53% on FineLeanCorpus and 41.49% on NuminaMath-LEAN
• MathForm-8B achieves 88.06% Syntax Check and 72.37% Consistency Check Pass@8 across six benchmarks, outperforming ReForm-32B and Goedel-Formalizer-V2-32B at a quarter the size
• On the hardest FATE-H / FATE-X subsets it reaches 63% / 37%
Consistency Check, beating the strongest specialized baseline by 10 and 12 points

🔗 Resources
📄 Paper: http://arxiv.org/abs/2608.14221
📚 Dataset: http://huggingface.co/datasets/openbmb/FormalVerse
🤖 Model: http://huggingface.co/openbmb/MathForm-8B
💻 Code: http://github.com/openbmb/MathForm