# GFLean: An Autoformalisation Framework for Lean via GF

arXiv: https://arxiv.org/abs/2404.01234 · HTML: https://mlsanity.com/paper/2404.01234/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 28 references that are in the map.
- First posted on arXiv 1 Apr 2024.

## Builds on (most cited first, 7 of 7)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [Formalising perfectoid spaces](https://mlsanity.com/paper/1910.12320/) (2019)
- [Formalising the h-principle and sphere eversion](https://mlsanity.com/paper/2210.07746/) (2022)

## Built on by (most cited first, 9 of 9)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [Customize Segment Anything Model for Multi-Modal Semantic Segmentation with Mixture of LoRA Experts](https://mlsanity.com/paper/2412.04220/) (2024)
- [Automated Formalization via Conceptual Retrieval-Augmented LLMs](https://mlsanity.com/paper/2508.06931/) (2025)
- [KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment](https://mlsanity.com/paper/2507.08665/) (2025)
- [TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition](https://mlsanity.com/paper/2510.11944/) (2025)
- [Symbolic Informalization: Fluent, Productive, Multilingual](https://mlsanity.com/paper/2606.16893/) (2026)
- [Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics](https://mlsanity.com/paper/2606.17581/) (2026)

## Abstract (arXiv)

We present an autoformalisation framework for the Lean theorem prover, called GFLean. GFLean uses a high-level grammar writing tool called Grammatical Framework (GF) for parsing and linearisation. GFLean is implemented in Haskell. We explain the functionalities of GFLean, its inner working and discuss its limitations. We also discuss how we can use neural network based translation programs and rule based translation programs together complimenting each other to build robust autoformalisation frameworks.