ProofNet 建立本科数学 autoformalization + theorem proving benchmark，把自然语言→Lean 正式变成独立研究任务

Azerbayev 等发布 ProofNet，一个面向 undergraduate-level mathematics 的 benchmark，包含自然语言题目、对应 Lean statements 与形式证明任务，用于同时评测 autoformalization 与 automated theorem proving。项目还研究 informalization / backtranslation，并公开数据与评测代码。ProofNet 之后成为评估数学 LLM 是否真正理解并忠实形式化自然语言命题的重要基准。