NaturalProver 把数学参考文献检索引入自然语言 proof generation，首次展示可用的 next-step 建议与短证明

NaturalProver 研究自然数学语言中的 next-step suggestion 与 full proof generation，并让模型显式条件化于 theorem / definition 等 background references，可由检索或人类提供。论文在人类评测中优于 fine-tuned GPT-3；系统能够生成部分 2–6 步短证明，next-step suggestions 被大学数学学生评为正确且有用的比例超过 40%。