跳到主要内容
检索

# Mathlib数学库

2 篇关联报道

订阅更新
  1. arXiv

    自荐式方法选择让形式化证明器在Putnam上命中率从84.2%升至95.0%

    该工作把形式化证明中的方法选择重新表述为适用性判断问题，提出“自荐”机制：在一次批量调用中让库中每个方法合约针对当前目标提出它要处理的目标片段、要执行的动作及所需条件，再对含糊或无依据的提案降级排序；在Putnam 2015–2025上hit@5达95.0%，最强重排基线为84.2%，IMO ProofBench上为91.7%对88.3%。

    Tsinghua UniversityImperial College LondonUniversity of Illinois Urbana-Champaign
    Xiaopeng Yuan（第一作者）
    自荐式方法选择方法契约形式化定理证明Lean证明助手Mathlib数学库
  2. arXiv

    Lean Pool：由 AI 代理维护的形式化数学档案库

    Lean Pool 是一个由 AI 代理生长、维护与优化的形式化数学仓库，论文报告其截至 2026 年 9 月 21 日已汇集 211 个已完成项目、3,228,485 行 Lean 代码、18 位提交贡献者，并通过代理辅助的依赖升级、证明压缩与数学评审来维持这些独立开发的形式化成果在 Lean/Mathlib 演进中持续可用。

    University of Washington
    Vasily Ilin（第一作者、通讯作者）
    Lean Pool形式化数学档案库AI智能体Lean证明助手Mathlib数学库形式化定理证明

已读完全部报道