General-purpose coding agents use standard shell and file interactions, yet formal theorem-proving agents often rely on specialized, ad-hoc tooling. This makes it difficult to determine which components of theorem-proving agents provide benchmark gains: an improved base model, a specialized harness, a specific tool, or a combination of any of them. We introduce mini-Lean-agent, a deliberately minimal agent for Lean tasks whose only model-visible tool is bash. The model must use bash to inspect and edit the repository, search local libraries, invoke Lean, and manage its own intermediate work, while a separate trusted evaluator verifies the final artifact. We compare mini-Lean-agent against AxProverBase and Numina-Lean-Agent on the Putnam 2025 benchmark. Experiments with Gemini 3.8 Flash as the base model show that mini-Lean-agent solves 7/12 problems at \$2 per problem limit, compared with AxProverBase's 4/12. With Astra as the base model, mini-Lean-agent solves 12/12 problems at an average cost of \$1.28 per problem. This suggests that a generic coding agent with a minimal harness can already achieve strong performance on Lean benchmarks. Our results motivate using mini-Lean-agent as a standard baseline when evaluating theorem-proving infrastructure.
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
Axiomatic_AI（公理人工智能）；Massachusetts Institute of Technology (MIT)（麻省理工学院）；Institut de Ciències Fotòniques (ICFO)（光子科学研究所）；Institució Catalana de Recerca i Estudis Avançats (ICREA)（加泰罗尼亚高级研究与高等学院）
Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
The University of Tokyo, Tokyo, Japan（东京大学）；National Institute of Informatics, Tokyo, Japan（日本信息处理学会）；Research and Development Center for Large Language Models, National Institute of Informatics, Tokyo, Japan（大型语言模型研究开发中心）；Kyoto University, Kyoto, Japan（京都大学）；Shiga University, Shiga, Japan（滋贺大学）；RIKEN Center for Advanced General Intelligence for Science Program, Kobe, Japan（理化学研究所高级一般智能科学项目中心）；National Institute of Science Technology Policy (NISTEP), Tokyo, Japan（科学与技术政策国立研究所）
TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
Skolkovo Institute of Science and Technology（斯科尔科沃科学技术研究所）；HSE University（高等经济大学）；Artificial Intelligence Research Institute（人工智能研究所）；Sberbank（俄罗斯联邦储蓄银行）
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
State Key Laboratory for Multimedia Information Processing, School of Computer Science, PKU-Anker LLM Lab, Peking University（信息处理国家重点实验室，计算机科学学院，PKU-Anker LLM实验室，北京大学）；Huawei Technologies Co., Ltd.（华为技术有限公司）；School of Software & Microelectronics, Peking University（软件与微电子学院，北京大学）；School of Electronics Engineering and Computer Science, Peking University（电子工程与计算机科学学院，北京大学）
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
School of Mathematical Sciences, Peking University（北京大学数学科学学院）；IQuest Research（IQuest研究院）；Research Institute for Mathematical Sciences, Kyoto University（京都大学数学研究所）；Westlake Institute for Advanced Study, Westlake University（西湖研究所在线高级研究院）；Beijing International Center for Mathematical Research and the New Cornerstone Science Laboratory, Peking University（北京国际数学研究中心和新基石科学实验室，北京大学）；Center for Machine Learning Research, Peking University（北京大学机器学习研究中心）；Center for Intelligent Computing, Great Bay Institute for Advanced Study, Great Bay University（智能计算中心，Great Bay高级研究院，Great Bay大学）；Zhongguancun Academy（中关村学院）
Proof Artifact Co-training for Theorem Proving with Language Models
University of Pittsburgh（匹兹堡大学）；OpenAI；IBM Research（IBM研究院）；Google Research（谷歌研究院）；Stanford University（斯坦福大学）；Carnegie Mellon University（卡内基梅隆大学）；CIBO Technologies（CIBO科技）；University of Toronto（多伦多大学）；University of Cambridge（剑桥大学）
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
University of Cambridge（剑桥大学）；University of Warsaw（华沙大学）；IDEAS NCBR（IDEAS国家生物医学研究中心）；Polish Academy of Sciences（波兰科学院）；Google Research（谷歌研究院）；Stanford University（斯坦福大学）
Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover
Princeton Language and Intelligence（普林斯顿语言与智能）；Amazon（亚马逊）；Department of Computer Science, University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校计算机科学系）
