AnnalsChallenge 发布论文：50 个《数学年刊》近年主定理被人工形式化为 Lean benchmark，并以 AI 审计语义

Browning 等于 10 月 13 日发布 AnnalsChallenge 论文：从 2020 年以来《Annals of Mathematics》的 207 篇论文中筛选并手工形式化 50 个 main theorem statements，建立在 Lean 4 / Mathlib 上；每个 statement 都经过人工 review，并再次用 AI audit，必要时还咨询原论文作者。论文不提供 gold proofs，而是把这些可信 research-level statements 作为 proving benchmark。作者报告截至 10 月 2 日的社区 LeanEval submissions 中已有 40/50 获 accepted proof，其中 Axiom Prover 覆盖全部 40；同时指出大量 differential / Riemannian geometry、Shimura varieties 等论文仍因 Mathlib 基础设施缺失而难以仅陈述主定理。