MathlibLemma 用 LLM 主动挖掘并形式化 Mathlib 中缺失的“民间引理”

MathlibLemma 构建了一个用于发现、形式化和证明可复用中间引理的 LLM pipeline，公开结果包括 1,506 个通过 Lean 检查和 proof-bypass screening 的证明，并构建了包含 4,028 个非平凡、type-checked Lean statements 的 benchmark；其中一小部分生成结果已被 Mathlib 接收。