NaturalProver conditions language-model proof generation on mathematical background references such as definitions and theorems, either retrieved automatically or supplied by humans.
The paper reported that NaturalProver improved next-step suggestions and full-proof generation over fine-tuned GPT-3 on NaturalProofs, generated some short 2–6 step proofs, and produced next-step suggestions judged correct and useful more than 40% of the time in human evaluation.
NaturalProver conditions language-model proof generation on mathematical background references such as definitions and theorems, either retrieved automatically or supplied by humans. The project studied both next-step suggestion and full-proof generation and released the NaturalProofs-Gen data, training and generation code, evaluation tooling and model assets.
The work helped establish natural-language theorem proving as a generative-model problem distinct from answer-only quantitative reasoning and formal proof search. Its grounding mechanism also made mathematical references explicit rather than leaving proof generation entirely inside an ungrounded language model.
Significance rationale: NaturalProver made next-step and full-proof generation in ordinary mathematical language an explicit language-model task and paired generation with retrieved or human-provided mathematical references, anticipating later retrieval-grounded mathematical reasoning systems.
—
The paper publicly reported the grounded proof-generation tasks, model and evaluation results. This research record alone does not imply independent verification of generated proofs.
The authors released a public repository containing NaturalProofs-Gen data, training and generation code, evaluation tooling and model assets. E3 records artifact inspectability, not mathematical certification of the generated proofs.
No corrections recorded.
