FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language
  Models
Formal mathematical reasoning remains a critical challenge for artificial
intelligence, hindered by limitations of existing benchmarks in scope and
scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark
comprising 5,560 formally verified problems spanning from high-school Olympiad
challenges to undergraduate-level theorems across diverse domains (e.g.,
algebra, applied mathematics, calculus, number theory, and discrete
mathematics). To mitigate the inefficiency of manual formalization, we
introduce a novel human-in-the-loop autoformalization pipeline that integrates:
(1) specialized large language models (LLMs) for statement autoformalization,
(2) multi-LLM semantic verification, and (3) negation-based disproof filtering
strategies using off-the-shelf LLM-based provers. This approach reduces expert
annotation costs by retaining 72.09% of statements before manual verification
while ensuring fidelity to the original natural-language problems. Our
evaluation of state-of-the-art LLM-based theorem provers reveals significant
limitations: even the strongest models achieve only 16.46% success rate under
practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling
in algebra but failing in calculus) and over-reliance on simplified automation
tactics. Notably, we identify a counterintuitive inverse relationship between
natural-language solution guidance and proof success in chain-of-thought
reasoning scenarios, suggesting that human-written informal reasoning
introduces noise rather than clarity in the formal reasoning settings. We
believe that FormalMATH provides a robust benchmark for benchmarking formal
mathematical reasoning.
6819742e0d1c56fe9124fe3a
Zhouliang Yu
claimed_verified
2025-05-06T08:34:10.190Z
62a80fe3ac97233f1625235a
https://cdn-avatars.huggingface.co/v1/production/uploads/62a80fe3ac97233f1625235a/_rGtpqdY7OEBz3pyqb6fE.jpeg
Zhouliang Yu
user
zhouliang
6819742e0d1c56fe9124fe3b
Ruotian Peng
admin_assigned
2025-05-06T08:48:20.491Z
662f2c8435ab6df959b005de
/avatars/3e30053ecbe9cc14b5e1eb2b014755de.svg
ruotian peng
user
prt66
6819742e0d1c56fe9124fe3c
Keyi Ding
6819742e0d1c56fe9124fe3d
Yizhe Li
6819742e0d1c56fe9124fe3e
Zhongyuan Peng
claimed_verified
2025-07-09T15:10:48.399Z
63299f93688ad82b783aaf20
/avatars/7c11e60e551ef1c62aa2862529e357f5.svg
zhongyuan peng
user
happzy2633
6819742e0d1c56fe9124fe3f
Minghao Liu
claimed_verified
2025-05-06T08:33:31.975Z
6417d9ea8f689506e7148417
https://cdn-avatars.huggingface.co/v1/production/uploads/6417d9ea8f689506e7148417/bAYcruWNw4WvmuQcGgcwC.jpeg
minghao
user
Liam-Liu
6819742e0d1c56fe9124fe40
Yifan Zhang
admin_assigned
2025-05-06T14:10:20.040Z
647bf082aba7062fe5c51ca9
https://cdn-avatars.huggingface.co/v1/production/uploads/647bf082aba7062fe5c51ca9/p4lY9IjHiWZETKmFq1mtU.jpeg
Yifan Zhang
user
yifAI
6819742e0d1c56fe9124fe41
Zheng Yuan
admin_assigned
2025-05-06T08:49:20.735Z
649da6b4599302cdb9bc232b
https://cdn-avatars.huggingface.co/v1/production/uploads/noauth/DxQT6LCDTZvyGUUe2t19c.jpeg
Zheng Yuan
user
ZhengYuan
6819742e0d1c56fe9124fe42
Huajian Xin
admin_assigned
2025-05-06T08:49:28.104Z
6532a060a78e70d19c669103
/avatars/3cc9309b0e31da0fb83f1c3ef87dbe9f.svg
HuajianXin
user
HuajianXin
6819742e0d1c56fe9124fe43
Wenhao Huang
admin_assigned
2025-05-06T08:49:44.482Z
641e5bf65f274a0a92c2f6a2
/avatars/c15a54c51998c0e6367685e8e1737ec9.svg
Wenhao Huang
user
EZ-hwh
6819742e0d1c56fe9124fe44
Yandong Wen
admin_assigned
2025-05-06T08:49:51.642Z
643c21735fcffe09fb68a46f
/avatars/76aabacd318aa954d4c53094ad456056.svg
Yandong Wen
user
ydwen
6819742e0d1c56fe9124fe45
Ge Zhang
admin_assigned
2025-05-06T08:49:59.764Z
638efcf4c67af472d316d424
/avatars/97a57859d7d87a3a8f1bb41d32a72bc2.svg
Ge Zhang
user
zhangysk
6819742e0d1c56fe9124fe46
Weiyang Liu
admin_assigned
2025-05-06T08:50:07.063Z
648905d1a15c43c791d4381f
https://cdn-avatars.huggingface.co/v1/production/uploads/648905d1a15c43c791d4381f/GpqGBzsLiMHX0gWZEz3qn.jpeg
Weiyang Liu
user
wy1iu
FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language
  Models
Formal mathematical reasoning remains a critical challenge for artificial
intelligence, hindered by limitations of existing benchmarks in scope and
scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark
comprising 5,560 formally verified problems spanning from high-school Olympiad
challenges to undergraduate-level theorems across diverse domains (e.g.,
algebra, applied mathematics, calculus, number theory, and discrete
mathematics). To mitigate the inefficiency of manual formalization, we
introduce a novel human-in-the-loop autoformalization pipeline that integrates:
(1) specialized large language models (LLMs) for statement autoformalization,
(2) multi-LLM semantic verification, and (3) negation-based disproof filtering
strategies using off-the-shelf LLM-based provers. This approach reduces expert
annotation costs by retaining 72.09% of statements before manual verification
while ensuring fidelity to the original natural-language problems. Our
evaluation of state-of-the-art LLM-based theorem provers reveals significant
limitations: even the strongest models achieve only 16.46% success rate under
practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling
in algebra but failing in calculus) and over-reliance on simplified automation
tactics. Notably, we identify a counterintuitive inverse relationship between
natural-language solution guidance and proof success in chain-of-thought
reasoning scenarios, suggesting that human-written informal reasoning
introduces noise rather than clarity in the formal reasoning settings. We
believe that FormalMATH provides a robust benchmark for benchmarking formal
mathematical reasoning.
FormalMATH, a large-scale Lean4 benchmark, introduces an autoformalization pipeline to reduce manual annotation costs and identifies limitations of existing LLM-based theorem provers in formal mathematical reasoning.
Lean4 autoformalization large language models multi-LLM semantic verification negation-based disproof filtering formal mathematical reasoning theorem provers domain bias chain-of-thought reasoning