DeepSeek-V3 first decomposes problems into subgoals; successful subgoal proofs become cold-start reasoning traces for reinforcement learning.
DeepSeek-Prover-V2-671B reported 88.9% on miniF2F-test and solved 49 of 658 PutnamBench problems.
The design made informal planning an explicit training scaffold for high-capacity formal theorem provers.
Significance rationale: DeepSeek-Prover-V2 narrowed the gap between natural-language reasoning and formal proof generation at much larger scale.
—
—
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
No corrections recorded.
