LeanDojo 发布：首次为 Lean 提供可编程交互环境、可复现数据抽取与 retrieval-augmented theorem proving 栈

Yang 等发布 LeanDojo，一个用于与 Lean theorem prover 交互、抽取 proof states / tactics / dependency data、复现实验并训练 neural theorem provers 的开放平台。配套 ReProver 使用 premise retrieval + language model proof generation，在 Lean 上展示 retrieval-augmented theorem proving；项目同时提供可版本化的数据抽取工具，降低 Mathlib 演化导致实验不可复现的问题。