本文介绍了LeanDojo，一个开源的交互式证明环境，以及其衍生的ReProver程序，能够有效选择定理前提。研究还提出了基于大型语言模型的数学推理工具，如InternLM-Math和Lean Copilot，展示了合成数据在定理证明中的潜力，并优化了形式证明的可读性和简洁性。此外，LeanAgent通过终身学习框架提升了高等数学定理证明的适应性和性能。