---
title: "GFLean: An Autoformalisation Framework for Lean via GF (2024)"
description: "GFLean is a rule-based tool that converts simple English mathematical statements into… 65% accuracy. 26 references, cited by 5 papers here."
authors: ["Shashank Pathak"]
year: 2024
venue: "arXiv:2404.01234"
source: "https://arxiv.org/abs/2404.01234"
doi: "10.48550/arxiv.2404.01234"
arxiv: "2404.01234"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/pathak-2024-gflean-autoformalisation-framework-lean-gf/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/pathak-2024-gflean-autoformalisation-framework-lean-gf/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/11/) / GFLean: An Autoformalisation Framework for Lean via GF

# GFLean: An Autoformalisation Framework for Lean via GF

**Authors:** Shashank Pathak · **Year:** 2024 · **Venue:** arXiv:2404.01234 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 0 citations (OpenAlex, 2026-10-14) · 5 in our library, of the 149,439 papers whose bibliographies we read

## Summary
GFLean is a rule-based tool that converts simple English mathematical statements into input for the Lean theorem prover. Its input language, Simplified ForTheL, is derived from the controlled natural language ForTheL and its existing GF implementation. ForTheL maps to first-order formulas, but the author gives Simplified ForTheL a type-theoretic semantics that fits Lean.

The pipeline has three stages:
- Grammatical Framework (GF) parses the input.
- Haskell performs the non-compositional abstract syntax tree (AST) transformations that GF cannot express.
- A separately written GF grammar for Lean expressions linearises the result.

Only statements are formalised, not proofs. The output is a Lean declaration with the proof left as `sorry`.

For evaluation, the tool was run on statements drawn from Chartrand, Polimeni and Zhang's *Mathematical Proofs*, specifically its Chapter 3. After light rewording, it handled 42 of the 62 statements. The author takes this as early evidence that GF suits modular, potentially scalable rule-based autoformalisation. The paper also argues that rule-based back-translation could let users check neural formalisations themselves, without needing a domain expert.

## Key points
- **Architecture:** GF handles parsing and output, while Haskell manipulates the ASTs in between. Minor pre-processing lowercases the input. Post-processing cleans up whitespace and gives each hypothesis a unique name.
- **Textbook coverage:** 42 of 62 statements were formalised. The other 20 would need a larger lexicon and support for phenomena such as postfix quantification of symbols and donkey anaphora.
- **Grammar and lexicon limitations:**
  - The lexicon is tiny.
  - There is no support for conjoined predicates or terms, or for several adjectives on one noun.
  - Singular and plural forms are not distinguished, so some ungrammatical input is accepted.
- **No extensibility:** GF grammars cannot be extended at run-time, so user definitions must be hard-coded. GFLean also never interacts with Lean itself.
- **Context and future work:**
  - The paper cites a neural baseline in which Codex formalised 120 statements into Lean with 65% accuracy.
  - Planned extensions include richer concrete syntaxes (records, tables, parameters), moving to full ForTheL, and a bigger lexicon.
  - The author also suggests reimplementing GFLean in Lean through its metaprogramming features.
  - The code is available on GitHub.

*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

- [University of Manchester](https://md.research.elamur.ai/free/en/universities/university-of-manchester/) — University, Manchester, United Kingdom · 87 works · 44,938 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 16,667 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 16,194 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 16,039 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 15,891 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 252 works

## Cite

Cite as: Shashank Pathak. 2024. GFLean: An Autoformalisation Framework for Lean via GF. arXiv:2404.01234.

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

```bibtex
@misc{pathak2024gflean,
  title = {{GFLean: An Autoformalisation Framework for Lean via GF}},
  author = {Shashank Pathak},
  year = {2024},
  doi = {10.48550/arxiv.2404.01234},
  eprint = {2404.01234},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2404.01234}
}
```

- [← previous Gender Bias Evaluation in Machine Translation for Amharic, Tigrigna, and Afaan Oromoo](https://md.research.elamur.ai/free/en/papers/sewunetie-2024-gender-bias-evaluation-machine-translation/)
- [next → HATFormer: Historic Handwritten Arabic Text Recognition with Transformers](https://md.research.elamur.ai/free/en/papers/chan-2024-hatformer-historic-handwritten-arabic-text/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/11/)

## References

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

1. [https://github.com/pkshashank/GFLeanTransfer](https://github.com/pkshashank/GFLeanTransfer) [↗](https://github.com/pkshashank/GFLeanTransfer)
2. [https://www.isa-afp.org/](https://www.isa-afp.org/) [↗](https://www.isa-afp.org/)
3. [https://github.com/leanprover-community/mathlib4](https://github.com/leanprover-community/mathlib4) [↗](https://github.com/leanprover-community/mathlib4)
4. [https://leanprover-community.github.io/mathlib_stats.html](https://leanprover-community.github.io/mathlib_stats.html) [↗](https://leanprover-community.github.io/mathlib_stats.html)
5. Achiam, J., Adler, S., Agarwal, S., Ahmad, L., Akkaya, I., Aleman, F.L., Almeida, D., Altenschmidt, J., Altman, S., Anadkat, S., et al.: [Gpt-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv preprint arXiv:2303.08774 (2023)
6. Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: Proceedings of the 9th ACM SIG-PLAN International Conference on Certified Programs and Proofs. pp. 299–312 (2020) [find](https://scholar.google.com/scholar?q=Buzzard%2C+K%2E%2C+Commelin%2C+J%2E%2C+Massot%2C+P%2E%3A+Formalising+perfectoid+spaces%2E+In%3A+Proceedings+of+the+9th+ACM+SIG%2DPLAN+International+Conference+on+Certified+Programs+and+Proofs%2E+pp%2E+299%E2%80%93312+%282020%29)
7. Chartrand, G., Polimeni, A.D., Zhang, P.: Mathematical proofs. chap. 3, pp. 81–104. Pearson (2017) [find](https://scholar.google.com/scholar?q=Chartrand%2C+G%2E%2C+Polimeni%2C+A%2ED%2E%2C+Zhang%2C+P%2E%3A+Mathematical+proofs%2E+chap%2E+3%2C+pp%2E+81%E2%80%93104%2E+Pearson+%282017%29)
8. De Lon, A., Koepke, P., Lorenzen, A., Marti, A., Schütz, M., Wenzel, M.: The isabelle/naproche natural language proof assistant. In: Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28. pp. 614–624. Springer International… [find](https://scholar.google.com/scholar?q=De+Lon%2C+A%2E%2C+Koepke%2C+P%2E%2C+Lorenzen%2C+A%2E%2C+Marti%2C+A%2E%2C+Sch%C3%BCtz%2C+M%2E%2C+Wenzel%2C+M%2E%3A+The+isabelle%2Fnaproche+natural+language+proof+assistant%2E+In%3A+Automated+Deduction%E2%80%93CADE+28%3A+28th+International+Conference+on+Autom)
9. van Doorn, F., Massot, P., Nash, O.: Formalising the h-principle and sphere eversion. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 121–134 (2023) [find](https://scholar.google.com/scholar?q=van+Doorn%2C+F%2E%2C+Massot%2C+P%2E%2C+Nash%2C+O%2E%3A+Formalising+the+h%2Dprinciple+and+sphere+eversion%2E+In%3A+Proceedings+of+the+12th+ACM+SIGPLAN+International+Conference+on+Certified+Programs+and+Proofs%2E+pp%2E+121%E2%80%93134+%2820)
10. Gadgil, S., Tadipatri, A.R., Agrawal, A., Narayanan, A., Goyal, N.: Towards automating formalisation of theorem statements using large language models. In: 36th Conference on Neural Information Processing Systems (NeurIPS 2022) Workshop on MATH-AI (2022) [find](https://scholar.google.com/scholar?q=Gadgil%2C+S%2E%2C+Tadipatri%2C+A%2ER%2E%2C+Agrawal%2C+A%2E%2C+Narayanan%2C+A%2E%2C+Goyal%2C+N%2E%3A+Towards+automating+formalisation+of+theorem+statements+using+large+language+models%2E+In%3A+36th+Conference+on+Neural+Information+Proces)
11. Ganesalingam, M.: The language of mathematics. Springer (2013) [find](https://scholar.google.com/scholar?q=Ganesalingam%2C+M%2E%3A+The+language+of+mathematics%2E+Springer+%282013%29)
12. Humayoun, M., Raffalli, C.: Mathnat-mathematical text in a controlled natural language. Special issue: Natural Language Processing and its Applications 46, 293–307 (2010) [find](https://scholar.google.com/scholar?q=Humayoun%2C+M%2E%2C+Raffalli%2C+C%2E%3A+Mathnat%2Dmathematical+text+in+a+controlled+natural+language%2E+Special+issue%3A+Natural+Language+Processing+and+its+Applications+46%2C+293%E2%80%93307+%282010%29)
13. Jiang, A.Q., Li, W., Jamnik, M.: Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755 (2023) [find](https://scholar.google.com/scholar?q=Jiang%2C+A%2EQ%2E%2C+Li%2C+W%2E%2C+Jamnik%2C+M%2E%3A+Multilingual+mathematical+autoformalization%2E+arXiv+preprint+arXiv%3A2311%2E03755+%282023%29)
14. Kamp, H., Van Genabith, J., Reyle, U.: Discourse representation theory. In: Handbook of Philosophical Logic: Volume 15, pp. 125–394. Springer (2010) [find](https://scholar.google.com/scholar?q=Kamp%2C+H%2E%2C+Van+Genabith%2C+J%2E%2C+Reyle%2C+U%2E%3A+Discourse+representation+theory%2E+In%3A+Handbook+of+Philosophical+Logic%3A+Volume+15%2C+pp%2E+125%E2%80%93394%2E+Springer+%282010%29)
15. Moura, L.d., Ullrich, S.: The lean 4 theorem prover and programming language. In: Automated Deduction– CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, [Proceedings 28](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/). pp. 625–635. Springer (2021)
16. Ranta, A.: Grammatical framework: Programming with multilingual grammars, vol. 173. CSLI Publications, Center for the Study of Language and Information Stanford (2011) [find](https://scholar.google.com/scholar?q=Ranta%2C+A%2E%3A+Grammatical+framework%3A+Programming+with+multilingual+grammars%2C+vol%2E+173%2E+CSLI+Publications%2C+Center+for+the+Study+of+Language+and+Information+Stanford+%282011%29)
17. Ranta, A.: Translating between language and logic: what is easy and what is difficult. In: Automated Deduction– CADE-23: 23rd International Conference on Automated Deduction, Wrocław, Poland, July 31-August 5, 2011. Proceedings 23. pp. 5–25. Springer (2011) [find](https://scholar.google.com/scholar?q=Ranta%2C+A%2E%3A+Translating+between+language+and+logic%3A+what+is+easy+and+what+is+difficult%2E+In%3A+Automated+Deduction%E2%80%93+CADE%2D23%3A+23rd+International+Conference+on+Automated+Deduction%2C+Wroc%C5%82aw%2C+Poland%2C+July+31%2D)
18. Ranta, A., Angelov, K., Gruzitis, N., Kolachina, P.: [Abstract syntax as interlingua: Scaling up the grammatical framework from controlled languages to robust pipelines](https://md.research.elamur.ai/free/en/papers/ranta-2020-abstract-syntax-as-interlingua-scaling/). Computational Linguistics 46(2), 425–486 (2020)
19. Schaefer, J.F., Amann, K., Kohlhase, M.: Prototyping controlled mathematical languages in jupyter notebooks. In: Mathematical Software–ICMS 2020: 7th International Conference, Braunschweig, Germany, July 13–16, 2020, Proceedings 7. pp. 406–415. Springer (2020) [find](https://scholar.google.com/scholar?q=Schaefer%2C+J%2EF%2E%2C+Amann%2C+K%2E%2C+Kohlhase%2C+M%2E%3A+Prototyping+controlled+mathematical+languages+in+jupyter+notebooks%2E+In%3A+Mathematical+Software%E2%80%93ICMS+2020%3A+7th+International+Conference%2C+Braunschweig%2C+Germany%2C+J)
20. Schaefer, J.F., Kohlhase, M.: The glif system: A framework for inference-based natural-language understanding (2020) [find](https://scholar.google.com/scholar?q=Schaefer%2C+J%2EF%2E%2C+Kohlhase%2C+M%2E%3A+The+glif+system%3A+A+framework+for+inference%2Dbased+natural%2Dlanguage+understanding+%282020%29)
21. Verchinine, K., Lyaletski, A., Paskevich, A.: System for automated deduction (sad): a tool for proof verification. In: International Conference on Automated Deduction. pp. 398–403. Springer (2007) [find](https://scholar.google.com/scholar?q=Verchinine%2C+K%2E%2C+Lyaletski%2C+A%2E%2C+Paskevich%2C+A%2E%3A+System+for+automated+deduction+%28sad%29%3A+a+tool+for+proof+verification%2E+In%3A+International+Conference+on+Automated+Deduction%2E+pp%2E+398%E2%80%93403%2E+Springer+%282007%29)
22. Vershinin, K., Paskevich, A.: Forthel—the language of formal theories. International Journal of Information Theories and Applications 7(3), 120–126 (2000) [find](https://scholar.google.com/scholar?q=Vershinin%2C+K%2E%2C+Paskevich%2C+A%2E%3A+Forthel%E2%80%94the+language+of+formal+theories%2E+International+Journal+of+Information+Theories+and+Applications+7%283%29%2C+120%E2%80%93126+%282000%29)
23. Wang, Q., Brown, C., Kaliszyk, C., Urban, J.: Exploration of neural machine translation in autoformalization of mathematics in mizar. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 85–98 (2020) [find](https://scholar.google.com/scholar?q=Wang%2C+Q%2E%2C+Brown%2C+C%2E%2C+Kaliszyk%2C+C%2E%2C+Urban%2C+J%2E%3A+Exploration+of+neural+machine+translation+in+autoformalization+of+mathematics+in+mizar%2E+In%3A+Proceedings+of+the+9th+ACM+SIGPLAN+International+Conference+on)
24. Wang, Q., Kaliszyk, C., Urban, J.: First experiments with neural translation of informal to formal mathematics. In: Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11. pp. 255–270. Springer (2018) [find](https://scholar.google.com/scholar?q=Wang%2C+Q%2E%2C+Kaliszyk%2C+C%2E%2C+Urban%2C+J%2E%3A+First+experiments+with+neural+translation+of+informal+to+formal+mathematics%2E+In%3A+Intelligent+Computer+Mathematics%3A+11th+International+Conference%2C+CICM+2018%2C+Hagenber)
25. Wu, Y., Jiang, A.Q., Li, W., Rabe, M., Staats, C., Jamnik, M., Szegedy, C.: [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). Advances in Neural Information Processing Systems 35, 32353–32368 (2022)
26. Zinn, C.: Understanding informal mathematical discourse. PhD thesis, Institut fur Informatik, Universitat Erlangen-Nurnberg (2004) [find](https://scholar.google.com/scholar?q=Zinn%2C+C%2E%3A+Understanding+informal+mathematical+discourse%2E+PhD+thesis%2C+Institut+fur+Informatik%2C+Universitat+Erlangen%2DNurnberg+%282004%29)

*Updated 30 October 2026*