AlphaProof Code vs MathForm-8B: Two Stages of the Same Lean Pipeline, Not Two Rivals

Read the AlphaProof Code paper closely and a number jumps out that the announcement does not emphasise: of the four weeks DeepMind's five researchers spent verifying Signal, the part that could not be automated was the front. Human experts sat with a mixture of models to translate Signal's security goals into formal Lean specifications, and an expert reviewed every single one before any proof work started. That is the bottleneck. MathForm-8B, OpenBMB's 8-billion-parameter autoformalization model released on Hugging Face on 14 August 2026, is a direct attempt to automate exactly that step — taking a natural-language mathematical statement and emitting a Lean 4 theorem statement ready for someone else to prove. Set them side by side and you are not comparing two products. You are looking at two consecutive stages of one pipeline, separated by the difference between mathematics and protocol security.

The pipeline, in the order the work happens

Formal verification of real software has three jobs. First, decide what must be true and write it down in a formal language. Second, prove that the implementation satisfies it. Third, check the proofs mechanically, because a wrong proof is worse than no proof.

MathForm-8B does job one, for a narrow input class: textbook-style mathematical claims. Give it "for every real number x, x² is non-negative" and it returns the imports, the types and a theorem header in Lean 4. What it does not return is a proof, and its authors are explicit that proof search is somebody else's problem. Its reported numbers, all vendor-reported and unreproduced, are 88.06% average Pass@8 under a syntax check and 72.37% under the stricter consistency check across six benchmarks — the gap between those two figures is the honest measure of how often a syntactically valid statement means something different from what was asked.

AlphaProof Code does jobs two and three, plus a specification stage that MathForm-8B could not touch. The Signal security goals are not mathematical claims in the sense MathForm was trained on; they are statements about a protocol — that messages stay protected before and after a device is temporarily compromised, that the initiator and responder are who they claim to be. Turning those into Lean required protocol expertise that no 8B autoformalizer holds. Once the specification existed, the proof work was handed entirely to agents, and the checking was handed to Lean's kernel plus a gatekeeper agent using comparator against a held-out spec copy.

What each one actually costs you to use

• Weights — MathForm-8B: downloadable, Apache 2.0, four safetensors shards in BF16, fine-tuned from Qwen3-8B. AlphaProof Code: none. The release is a Lean development, an AArch64 semantics and a libsignal binding at github.com/google-deepmind/code-verification.

• Running it — MathForm-8B: Transformers, vLLM or SGLang, all exposing an OpenAI-compatible endpoint, on hardware you own. AlphaProof Code: no endpoint, no API, no waitlist, no price; it is a research framework that DeepMind says needs "continued research" before it scales.

• Input — MathForm-8B: a natural-language math statement. AlphaProof Code: a formal specification plus the binary you want proved against it.

• Output — MathForm-8B: a Lean 4 theorem statement, unproved. AlphaProof Code: a machine-checked proof, or a refutation when the code is broken.

• Human review — MathForm-8B: you review the emitted statement, and at 72.37% consistency you will be reviewing a lot of them. AlphaProof Code: experts review every specification before proof work begins, then agents flag about 1% of the codebase for a second look.

• Known limits — MathForm-8B: math statements only, no proof generation, and the code repository linked in its README was still a placeholder at release. AlphaProof Code: no post-quantum guarantee for SPQR healing, no payload privacy, one session per promotion, and a MAC forgery bound that goes vacuous near 25,000 messages in a single session.

The gap MathForm-8B would have to close

It is tempting to say an autoformalizer could have written Signal's specifications and saved the researchers their front-loaded weeks. The paper's own account says otherwise, and the reason is specific. A specification of a protocol is not a restatement of a claim; it is a choice about adversary model. The Signal work carries a symbolic track in Dolev–Yao with a quantum attacker who breaks Diffie–Hellman after the handshake, and a computational track with classical adversaries and a concrete bound. Those two tracks state different theorems about the same code, and picking between them is an engineering decision with security consequences. No model that has been trained to turn "show that x² ≥ 0" into Lean is going to make that call.

What an autoformalizer plausibly could do is the mechanical part of that work: given a prose security goal and a library of existing Lean definitions, produce a first draft of the statement in the project's own idiom, for an expert to correct. That is a real saving and a much smaller one than the headline suggests. The paper reports a spec-deviation catalogue of over 200 computational entries and about 35 symbolic ones — fifteen of them gaps or bugs in the Double Ratchet analysis — which is what the human review step found. A model that drafts statements would have to be measured against that catalogue, not against a Pass@8 score on math benchmarks.

Where the two numbers are not comparable at all

MathForm-8B's 88.06% and AlphaProof Code's 6.5 million lines measure different things and should never be placed in the same column. One is a hit rate on a benchmark suite the authors built; the other is a quantity of proof produced for one target. The vendor is candid that the 88.06% uses a syntax check, which is a weak criterion — a statement can compile and still formalize the wrong claim, which is why the consistency figure is 16 points lower.

The AlphaProof Code figure with a comparable flavour is the validation work: two previously fixed Signal bugs, a weak-state bug and a small-subgroup bug, were reintroduced into an isolated copy, and in both cases the system produced a machine-checked proof that the buggy version fails the security theorem. That is a negative test, and a negative test is what an autoformalizer benchmark is missing entirely. MathForm-8B reports no result of the form "given a deliberately wrong statement, the model said so."

How you would actually use them together

Concretely, and this is the only part of the comparison with a near-term path: use an autoformalizer to draft, a strong general model to critique the draft, and a proof agent to attempt the proof. Each stage has a different failure mode, and routing all three through one key is the practical convenience. On OrcaRouter, more than 200 models sit behind a single API at provider list price with 0% markup, so a spec-drafting loop that sends the same statement to two models and diffs their Lean is a routing-DSL call rather than three contracts and three SDKs. Automatic failover covers the case where the model you picked is having a bad afternoon.

What none of that supplies is the guarantee. MathForm-8B gives you a statement, the models give you a critique, and something still has to prove it. At present the only published system that closes that loop on real deployed code is AlphaProof Code, and it is not for sale.

The reason to read both papers rather than pick a winner

MathForm-8B is a useful artifact with a narrow job and a real, measured accuracy ceiling. AlphaProof Code is a workflow demonstration whose most transferable finding is not the proof volume but the split: specification work wants humans and a strong general model, proof work wants agent teams and a kernel, and the boundary between them is where all the difficulty lives. Anyone building a verification pipeline should take the split seriously and treat autoformalization as the piece that reduces the cost of the first stage — not the piece that replaces it.

The honest summary for a team deciding what to download this month: MathForm-8B, yes, if you work with Lean and want a drafting aid. AlphaProof Code, read the artifact repository and the specification-deviation catalogue, because the catalogue tells you more about what formal verification of production code still cannot reach than any announcement will.