OpenBMB has fully open-sourced its MathForm pipeline for automated math formalization: the 8B model weights, a verified dataset of roughly 367,000 Lean 4 examples, evaluation code, and Pass@k scripts are all released together. The model is hosted on Hugging Face under an Apache 2.0 license, built on the Qwen3-8B base with BF16 weight precision. The project was completed by the OpenBMB team, jointly backed by Tsinghua University's NLP Lab and ModelBest (面壁智能), with the accompanying paper submitted to arXiv in mid-August, credited to 10 authors.
Automated formalization means translating a natural-language math statement into a machine-checkable formal language like Lean 4. The hard part isn't literal translation. Mathlib's type hierarchy and definitional system are enormous — a term like 'continuous function' or 'finite group' in a given statement has to be mapped precisely onto the one matching definition in the library, while making sure the formalized statement still means the same thing as the original. Get either step wrong, and the compiler may still nod along.
How the data was built
The MathForm pipeline has four stages. A planner first queries Mathlib for the mathematical concepts in a given statement, with the retrieval tool LeanExplore returning the top 22 results each time; the model then generates a Lean 4 statement conditioned on that retrieved context. Candidates go through format checking and compilation testing in turn, then a large-model judge makes a semantic-consistency call; passing trajectories are reconstructed backward into clean training traces.
One number in the paper makes the case for iteration: later rounds contributed an additional 31.0% of all retained samples. In other words, a single generation pass with no retries would have thrown away nearly a third of the usable data.
Retrieval is the most cost-effective part of the design. Asking a model to recall the exact name and signature of a Mathlib definition from memory is really testing whether it has memorized a library that keeps getting updated. Hand the library to a retrieval tool instead, and let the model just do the assembling, and the required parameter count naturally drops. That's also why an 8B model can go toe-to-toe with 32B ones: the two aren't really being tested on the same task.
The resulting dataset, called FormalVerse, contains roughly 367,000 verified samples drawn from DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath, and OpenR1-Math, supplemented with material from classic textbooks. The dataset has already picked up 358 likes on Hugging Face.
The scorecard, and its two readings
Training combines supervised fine-tuning followed by reinforcement learning. Evaluation spans six benchmarks: FormalMATH-Lite and DeepSeek-ProverBench cover competition math, CombiBench tests combinatorics, and the FATE series is split into M, H, and X tiers by algebraic difficulty.
MathForm-8B posts an average syntax-check Pass@8 of 88.06% and an average consistency-check score of 72.37%; the FATE tiers come in at 97.33%, 63.00%, and 37.00% for consistency, from M to X. The comparison set includes Herald Translator-7B, Kimina-Autoformalizer-7B, Mathesis-HPO-7B, along with the 7B/8B and 32B versions of StepFun-Formalizer, Goedel-Formalizer-V2, and ReForm. The 8B model surpasses several 32B dedicated formalization models across multiple test sets.
The gap between the two metrics is more revealing than either absolute score. Syntax checking only asks whether the code compiles; consistency checking asks whether the formalized statement actually means the same thing as the original problem. The 88% vs. 72% gap — those roughly fifteen points — is where this pipeline's real bottleneck currently sits. Something that compiles isn't necessarily the theorem you meant to prove.
The barrier to entry has dropped to a single workstation
This site recently covered Terence Tao's warning that AI could generate more proofs than anyone can read. Formalization is effectively the other half of the answer to that problem — as long as a proof passes the Lean compiler, whether a human can follow it is no longer a precondition for accepting it. The catch is that the statement itself has to be translated correctly first, and FATE-X's 37% shows there's still real distance to cover there.
Rough math: an 8B model loaded in BF16 needs about 16GB of VRAM; a 32B model at the same precision needs roughly 64GB. The former runs on a single 24GB consumer GPU; the latter needs multiple GPUs or professional-grade cards. For math departments, proof-assistant communities, and small teams, the hardware bar for running a formalization pipeline has dropped from cluster-scale to single-machine scale. With the dataset and evaluation scripts open too, the cost of reproducing or poking holes in the results has come down as well.
The list of names in the comparison table says something about how crowded this space has gotten: Herald, Kimina, Mathesis, StepFun-Formalizer, Goedel-Formalizer-V2, ReForm — all dedicated formalization models that have appeared in the past year or two, and all open-source. Formalization doesn't reward brute-forcing compute the way general-purpose chat does; what matters here is data-construction craft and a working verification loop, which makes parameter count a comparatively minor variable. Going from a paper demo to an open-source release is happening faster than most people would expect.
Sources: OpenBMB repository and model card, CocoLoop, arXiv preprint 2608.14221, Hugging Face dataset page; figures for parameter count, license, FormalVerse sample size, and per-benchmark Pass@8 methodology have been cross-checked.