---
title: "FIMO — paper by Liu et al. (2023) — summary and ideas"
description: "To build it, they converted the PDFs to LaTeX with the Mathpix tool and checked the output by hand. 16 references, cited by 44 papers here."
authors: ["Chengwu Liu", "Jianhao Shen", "Huajian Xin", "Zhengying Liu", "Ye Yuan", "Haiming Wang", "Wei Ju", "Chuanyang Zheng", "Yichun Yin", "Lin Li", "Ming Zhang", "Qun Liu"]
year: 2023
venue: "arXiv:2309.04295"
source: "https://arxiv.org/abs/2309.04295"
doi: "10.48550/arxiv.2309.04295"
arxiv: "2309.04295"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/liu-2023-fimo-challenge-formal-dataset-automated/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/liu-2023-fimo-challenge-formal-dataset-automated/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2023](https://md.research.elamur.ai/free/en/papers/2023/page/10/) / FIMO: A Challenge Formal Dataset for Automated Theorem Proving

# FIMO: A Challenge Formal Dataset for Automated Theorem Proving

**Authors:** Chengwu Liu, Jianhao Shen, [Huajian Xin](https://md.research.elamur.ai/free/en/authors/huajian-xin/), [Zhengying Liu](https://md.research.elamur.ai/free/en/authors/zhengying-liu/), [Ye Yuan](https://md.research.elamur.ai/free/en/authors/ye-yuan/), [Haiming Wang](https://md.research.elamur.ai/free/en/authors/haiming-wang/), [Wei Ju](https://md.research.elamur.ai/free/en/authors/wei-ju/), [Chuanyang Zheng](https://md.research.elamur.ai/free/en/authors/chuanyang-zheng/), [Yichun Yin](https://md.research.elamur.ai/free/en/authors/yichun-yin/), [Lin Li](https://md.research.elamur.ai/free/en/authors/lin-li/), [Ming Zhang](https://md.research.elamur.ai/free/en/authors/ming-zhang/) and [Qun Liu](https://md.research.elamur.ai/free/en/authors/qun-liu/) · **Year:** 2023 · **Venue:** arXiv:2309.04295 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2309.04295) · [PDF](https://arxiv.org/pdf/2309.04295v2) · [DOI 10.48550/arxiv.2309.04295](https://doi.org/10.48550/arxiv.2309.04295) · [arXiv 2309.04295](https://arxiv.org/abs/2309.04295) · [OpenAlex](https://openalex.org/W4386620158)

**Citations:** 9 citations (OpenAlex, 2026-10-14) · [44](https://md.research.elamur.ai/free/en/papers/liu-2023-fimo-challenge-formal-dataset-automated/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary

Neural provers built on large language models still rarely solve olympiad-grade problems. Formal data is scarce and costly to produce, existing benchmarks contain few truly hard items, and most formal datasets lack natural-language counterparts. The authors address this with FIMO, a Lean benchmark drawn from the IMO Shortlisted Problems (2006–2021), restricted to Algebra and Number Theory. To build it, they converted the PDFs to LaTeX with the Mathpix tool and checked the output by hand. They rephrased answer-type questions as provable claims. GPT-4 then generated the formalizations, revising its drafts using Lean error messages and human feedback, and every result was manually verified against the source problem. For baselines, GPT-4 wrote informal proofs (either supplied by humans or self-generated) and then turned them into formal Lean proofs. The approach reached over 20% Pass@8 on miniF2F but proved none of the FIMO statements. This shows that IMO-level formal reasoning remains far beyond current methods and gives the field a demanding, bilingual (formal and informal) testbed.

## Key points

- FIMO contains 149 Lean formal statements, each paired with an informal statement and a LaTeX informal proof. It is released on GitHub under the Apache License.
- The authors report that letting the LLM reflect on Lean checker errors and human comments substantially increased the share of problems that could be auto-formalized.
- GPT-4 baseline results:
  - On miniF2F-test, Pass@8 was 14.3% with human proofs and 20.9% with self-generated proofs.
  - On FIMO, it scored 0.0% in all settings.
  - Self-generated informal proofs gave better Pass@8, likely because they are more diverse.
- Error analysis found two main failure modes:
  - Model-written informal proofs were mostly mathematically wrong.
  - With human proofs, GPT-4 followed the reasoning but misapplied tactics such as `rw`.
  - Even so, its generated proofs averaged more than 11 lines, compared with under 3 for GPT-f.
- Limitations: the dataset excludes Combinatorics and Geometry, covers only shortlists from 2006–2021, and may contain a few residual formalization errors.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Peking University](https://md.research.elamur.ai/free/en/universities/peking-university/) — University, Beijing, China · 315 works · 43,267 citations
- [Chinese University of Hong Kong](https://md.research.elamur.ai/free/en/universities/chinese-university-of-hong-kong/) — University, Hong Kong, China · 159 works · 16,154 citations
- [Huawei Technologies](https://md.research.elamur.ai/free/en/companies/huawei-technologies/) — Company, Shenzhen, China · 96 works · 15,432 citations
- [Sun Yat-sen University](https://md.research.elamur.ai/free/en/universities/sun-yat-sen-university/) — University, Guangzhou, China · 72 works · 9,502 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 18,614 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 17,965 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 321 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

## Cite

Cite as: Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang and Qun Liu. 2023. FIMO: A Challenge Formal Dataset for Automated Theorem Proving. arXiv:2309.04295.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{liu2023fimo,
  title = {{FIMO: A Challenge Formal Dataset for Automated Theorem Proving}},
  author = {Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang and Qun Liu},
  year = {2023},
  doi = {10.48550/arxiv.2309.04295},
  eprint = {2309.04295},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2309.04295}
}
```

- [← previous DiscoScore: Evaluating Text Generation with BERT and Discourse Coherence](https://md.research.elamur.ai/free/en/papers/zhao-2023-discoscore-evaluating-text-generation-bert/)
- [next → Language acquisition: do children and language models follow similar learning stages?](https://md.research.elamur.ai/free/en/papers/evanson-2023-language-acquisition-children-language-models/)
- [↑ back to papers of 2023](https://md.research.elamur.ai/free/en/papers/2023/page/10/)

## References

16 references, 12 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Brown, T.; Mann, B.; Ryder, N.; Subbiah, M.; Kaplan, J. D.; Dhariwal, P.; Neelakantan, A.; Shyam, P.; Sastry, G.; Askell, A.; Agarwal, S.; Herbert-Voss, A.; Krueger, G.; Henighan, T.; Child, R.; Ramesh, A.; Ziegler, D.; Wu, J.; Winter, C.; Hesse, C.; Chen, M.; Sigler, E.; Litwin, M.; Gray, S.; Chess… — [Language Models are Few-Shot Learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/)
2. Han, J. M.; Rute, J.; Wu, Y.; Ayers, E. W.; and Polu, S. 2022. [Proof Artifact Co-training for Theorem Proving with Language Models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). arXiv:2102.06203.
3. Hendrycks, D.; Burns, C.; Kadavath, S.; Arora, A.; Basart, S.; Tang, E.; Song, D.; and Steinhardt, J. 2021. [Measuring Mathematical Problem Solving With the MATH Dataset](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/). NeurIPS.
4. Jiang, A.; Czechowski, K.; Jamnik, M.; Milos, P.; Tworkowski, S.; Li, W.; and Wu, Y. T. 2022a. [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/). In NeurIPS.
5. Jiang, A. Q.; Welleck, S.; Zhou, J. P.; Li, W.; Liu, J.; Jamnik, M.; Lacroix, T.; Wu, Y.; and Lample, G. 2022b. [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). In Submitted to The Eleventh International Conference on Learning Representations.
6. Koutsoukou-Argyraki, A. 2021. Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started. Jahresbericht der Deutschen Mathematiker-Vereinigung, 123(1): 3–26. mathlib Community, T. 2020. [The Lean Mathematical Library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). In Proceedin…
7. OpenAI. 2023. [GPT-4 Technical Report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv:2303.08774.
8. Polu, S.; Han, J. M.; Zheng, K.; Baksys, M.; Babuschkin, I.; and Sutskever, I. 2023. [Formal Mathematics Statement Curriculum Learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net.
9. Polu, S.; and Sutskever, I. 2020. [Generative Language Modeling for Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv:2009.03393.
10. Selsam, D.; Buzzard, K.; Barton, R.; Liang, P.; Loss, S.; and Wiedijk, F. 2020. IMO Grand Challenge. [find](https://scholar.google.com/scholar?q=Selsam%2C+D%2E%3B+Buzzard%2C+K%2E%3B+Barton%2C+R%2E%3B+Liang%2C+P%2E%3B+Loss%2C+S%2E%3B+and+Wiedijk%2C+F%2E+2020%2E+IMO+Grand+Challenge%2E)
11. Shen, J.; Yin, Y.; Li, L.; Shang, L.; Jiang, X.; Zhang, M.; and Liu, Q. 2021. Generate & Rank: A Multi-task Framework for Math Word Problems. In Findings of the Association for Computational Linguistics: EMNLP 2021, 2269–2279. Punta Cana, Dominican Republic: Association for Computational Linguistics… [find](https://scholar.google.com/scholar?q=Shen%2C+J%2E%3B+Yin%2C+Y%2E%3B+Li%2C+L%2E%3B+Shang%2C+L%2E%3B+Jiang%2C+X%2E%3B+Zhang%2C+M%2E%3B+and+Liu%2C+Q%2E+2021%2E+Generate+%26+Rank%3A+A+Multi%2Dtask+Framework+for+Math+Word+Problems%2E+In+Findings+of+the+Association+for+Computational+Linguisti)
12. Shinn, N.; Cassano, F.; Labash, B.; Gopinath, A.; Narasimhan, K.; and Yao, S. 2023. [Reflexion: Language Agents with Verbal Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/shinn-2023-reflexion-language-agents-verbal-reinforcement/). arXiv:2303.11366.
13. Szegedy, C. 2020. A Promising Path Towards Autoformalization and General Artificial Intelligence. In Benzmüller, C.; and Miller, B., eds., Intelligent Computer Mathematics, 3–20. Cham: Springer International Publishing. ISBN 978-3-030-53518-6. [find](https://scholar.google.com/scholar?q=Szegedy%2C+C%2E+2020%2E+A+Promising+Path+Towards+Autoformalization+and+General+Artificial+Intelligence%2E+In+Benzmu%CC%88ller%2C+C%2E%3B+and+Miller%2C+B%2E%2C+eds%2E%2C+Intelligent+Computer+Mathematics%2C+3%E2%80%9320%2E+Cham%3A+Springer+Inter)
14. Wang, H.; Yuan, Y.; Liu, Z.; Shen, J.; Yin, Y.; Xiong, J.; Xie, E.; Shi, H.; Li, Y.; Li, L.; Yin, J.; Li, Z.; and Liang, X. 2023. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. In Proceedings of the 61st Annual Meeting of the Association for Com… [find](https://scholar.google.com/scholar?q=Wang%2C+H%2E%3B+Yuan%2C+Y%2E%3B+Liu%2C+Z%2E%3B+Shen%2C+J%2E%3B+Yin%2C+Y%2E%3B+Xiong%2C+J%2E%3B+Xie%2C+E%2E%3B+Shi%2C+H%2E%3B+Li%2C+Y%2E%3B+Li%2C+L%2E%3B+Yin%2C+J%2E%3B+Li%2C+Z%2E%3B+and+Liang%2C+X%2E+2023%2E+DT%2DSolver%3A+Automated+Theorem+Proving+with+Dynamic%2DTree+Sampling+Guided)
15. Wu, Y.; Jiang, A. Q.; Li, W.; Rabe, M. N.; Staats, C.; Jamnik, M.; and Szegedy, C. 2022. [Autoformalization with Large Language Models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). arXiv:2205.12615.
16. Zheng, K.; Han, J. M.; and Polu, S. 2022. [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). arXiv:2109.00110.

*Updated 2 November 2026*