Intelai
AI Can Prove the Wrong Specification Perfectly
DeepSeek's prover is a real advance in Lean proofs. The bottleneck in critical systems is still the English sentence the proof must satisfy.
DeepSeek's Prover-V2 solves 88.9% of the MiniF2F-test and 49 of the 658 problems in PutnamBench. Those are strong numbers for automated theorem proving, and they are the least interesting thing about the model.
The interesting thing is what the numbers do not touch. A theorem prover can close a goal in seconds. It cannot tell you that the goal is the wrong one. In critical systems, the wrong goal is the expensive failure.
What the model does
Prover-V2 is a 671 billion parameter model trained to write proofs in Lean 4. It decomposes a theorem into subgoals, proves the pieces, and assembles them. The paper (opens in a new tab) describes a recursive pipeline that uses DeepSeek-V3 to generate the subgoal structure and a reinforcement learning stage to improve the proof search.
The benchmark results are real: 88.9% on MiniF2F-test, 49 of 658 on PutnamBench. The model is also open, which means a lab can download the weights and run them. That combination, strong results plus local execution, is why the release matters.
For a defense engineer, the appeal is obvious. Formal verification is expensive, and a large part of the cost is proof engineering: finding the lemma, trying the tactic, repairing the proof after a definition changes. A model that is good at proof search can compress that work.
The specification is the hard part
Formal verification proves that an implementation satisfies a specification. The proof is only as good as the specification. If the specification omits a failure mode, the proof is silent about it. If the specification encodes the wrong assumption, the proof certifies the wrong behavior.
That is not a hypothetical. It is the normal failure mode of formal methods. A team spends months proving a property, then discovers that the property does not cover the case that matters. The proof is valid. The system is still unsafe.
The translation from an English requirement to a formal statement is where the judgment lives. "The system shall maintain safe separation" has to become a predicate over states, inputs, timing, and failure modes. Someone has to decide what counts as separation, which failures are in scope, and what happens at the boundary. A prover can help explore the consequences of those choices. It cannot make them.
The proof checker is the trust anchor. The model is not.
The defense record shows why this is not a theoretical concern. Formal methods are already used in high-assurance work. DO-178C and its formal methods supplement, DO-333, recognize formal analysis for airborne software. The seL4 microkernel is a fully verified implementation, and it took years of expert effort. Those programs are evidence that verification works. They are also evidence that the expensive part is the specification and the proof engineering, not the final tactic.
That is why the Prover-V2 result is both important and easy to overread. It improves the part that was already mechanizable. It does not improve the part where a domain expert has to decide what must be true.
The same pattern shows up in cryptography and control systems. A verified implementation of a cipher is valuable. It does not tell you that the protocol using the cipher is sound. A verified controller is valuable. It does not tell you that the physical model in the specification matches the plant.
The provenance problem
There is a second limit, and it is practical. Prover-V2 comes from a Chinese lab. For work involving controlled unclassified information or classified data, the model is not something you can put into an accredited environment because the benchmark is good.
The issue is not the mathematics. It is the artifact. You need to know where the weights came from, what data shaped them, how updates are delivered, and whether you can reproduce a result six months later. Open weights help with inspection. They do not answer the supply chain question by themselves.
A lab can use the model for research. A program of record needs a provenance story, an evaluation record, and a maintenance path. Those are different standards, and the gap between them is where most AI tools stall.
The transferable asset is the method: subgoal decomposition, reinforcement learning for proof search, and a checker in the loop. Those techniques can be implemented on a model you can defend. The weights are not the strategy.
Where it helps now
The useful applications are narrower than "automated verification."
Use the model to repair proofs after a definition changes. Use it to search a bounded library for a lemma a human would take a day to find. Use it to draft regression proofs when a line of code moves. Use it to propose missing cases in a specification, then have a human decide which ones matter.
In each case, the model is inside a workflow with a checker and a reviewer. The checker verifies the proof. The reviewer verifies the statement. The model never becomes the authority.
That workflow is less exciting than a model that solves competition math. It is also the only version that survives an audit.
The question to ask
The right question about Prover-V2 is not whether it can prove a theorem. It can. The right question is whether your team can write a specification worth proving.
If the answer is no, the model will help you produce beautiful proofs of the wrong properties faster. If the answer is yes, it is a genuine force multiplier, and the bottleneck moves to the review of the statement, which is where it should have been all along.