MathlibLemma：民间引理生成与形式化数学基准

尽管 Lean 和 Mathlib 生态系统在大语言模型辅助下取得了显著成功，但缺乏许多民间引理仍是限制其作为日常工具可用性的障碍。为此，我们推出了 MathlibLemma，这是首个基于大语言模型的多智能体系统，旨在自动化发现和形式化数学民间引理。该系统通过主动挖掘缺失的数学连接结构，生成了经验证的引理库，部分已合并至最新 Mathlib 版本。此外，我们构建了包含 4028 个类型检查通过的 Lean 语句的基准测试集。这项工作将大语言模型从被动消费者转变为主动贡献者，确立了形式化数学库自我进化的建设性方法。