Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of declarative propositions, often neglecting the task of explicitly synthesizing solutions. This limitation is particularly acute in applied mathematics domains, where the goal is frequently to derive concrete values or executable algorithms rather than solely proving theorems. To address this, we introduce a Lean 4 framework that enforces a construction-verification workflow, compelling the agent to define explicit solutions before proving their correctness. We curate a comprehensive benchmark AMBER (Applied Mathematics BEnchmark for Reasoning) spanning core domains of applied mathematics, including convex analysis, optimization, numerical algebra, and high-dimensional probability. Aside from theorem proving, our benchmark features complex tasks such as evaluation, algorithm design, and representation transformation. Experiments reveal that current models face significant difficulties with these constructive tasks. Notably, we observe that general-purpose reasoning models consistently outperform specialized theorem provers. We attribute this to a degradation of instruction following capabilities in specialized models. Fine-tuning on proof corpora appears to induce ``tactical overfitting", compromising the ability to adhere to complex constructive requirements, whereas general models retain the versatility needed for multi-task formal reasoning.
From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory
School of Data Science, The Chinese University of Hong Kong, Shenzhen（香港中文大学深圳数据科学学院）；School of Science and Engineering, The Chinese University of Hong Kong, Shenzhen（香港中文大学深圳科学与工程学院）
Automated Tactics for Polynomial Reasoning in Lean 4
State Key Laboratory of Mathematical Sciences, Academy of Mathematics and Systems Science, University of Chinese Academy of Science（中国科学院数学与系统科学研究院）；Institute of Logic and Cognition, Department of Philosophy, Sun Yat-sen University（中山大学哲学系逻辑与认知研究所）
New York University（纽约大学）；Aarhus University（奥胡斯大学）；ETH Zurich（苏黎世联邦理工学院）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；Institute of Science and Technology Austria (ISTA)（奥地利科学技术研究所）；Chalmers（查尔姆斯理工大学）
Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse
State Key Lab of Processors, Institute of Computing Technology, CAS（处理器国家重点实验室，中国科学院计算技术研究所）；University of Chinese Academy of Sciences（中国科学院大学）；NorthChina University of Science and Technology（华北理工大学）
The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
Einstein Institute of Mathematics, The Hebrew University of Jerusalem（以撒·牛顿数学研究所，耶路撒冷希伯来大学）；Department of Mathematics, Imperial College London（伦敦帝国理工学院数学系）
FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups
MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
Department of Computer Science, University of Virginia（弗吉尼亚大学计算机科学系）；Astronomy , California Institute of Technology（加州理工学院天文学系）；Purdue University（普渡大学）；Massachusetts Institute of Technology（麻省理工学院）
Princeton University（普林斯顿大学）；University of Bonn（波恩大学）；University of Rennes（雷恩大学）；Utrecht University（乌得勒支大学）；Harmonic（哈莫尼克）；The Hague（海牙）；Eindhoven University of Technology（埃因霍温理工大学）；University of Massachusetts Lowell（马萨诸塞大学洛厄尔分校）；Baruch College（巴鲁克学院）；National University of Singapore（新加坡国立大学）
LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
Yau Mathematical Sciences Center, Tsinghua University（清华大学尤洋数学科学中心）；Iluvatar CoreX；Department of Mathematics, Southern University of Science and Technology（南方科技大学数学系）；Westlake Institute for Advanced Study, Westlake University（西湖研究学院）；Qiuzhen College, Tsinghua University（清华大学齐臻学院）；Department of Physics, The Chinese University of Hong Kong（香港中文大学物理系）；Yanqi Lake Beijing Institute of Mathematical Sciences and Applications (BIMSA)（燕琦湖北京应用数学研究所（BIMSA））
