arXivLean

Lean 4及配套数学库Mathlib已成为形式化数学的事实标准，arXivLean、PutnamBench等基准构建在其之上。

使用Claude Opus 5时，Maestro在arXivLean的2026年6月版本中自主发现了48个定理里34个的证明，而原生代理只做到19个。

arXivLean是从arXiv数学论文中提取定理并形式化得到的基准，属于研究级数学。