What changed
DeepSeek released 7B and 671B theorem-proving models, code and ProverBench for Lean 4. Its training pipeline used DeepSeek-V3 to decompose difficult problems into subgoals, translated successful pieces into formal proof traces and then applied reinforcement learning.
Why it matters
Formal proof assistants provide deterministic feedback, making theorem proving a useful test bed for teaching models to turn informal reasoning into machine-checkable results.
What to do
Try the 7B checkpoint on a small Lean repository with the compiler as the acceptance gate. Measure compiled proofs, repair iterations and test-time compute rather than trusting natural-language explanations.
Caveat
Benchmark results were author-reported and later papers improved on them. A Lean proof only establishes the encoded theorem from its assumptions; it does not verify that the formalization matches the real-world question.