mlsanityData to 14 Oct 2026

GFLean: An Autoformalisation Framework for Lean via GF

arXiv 2404.01234 ↗First posted 1 Apr 2024cs.CL math.LOcited by 9

Not on the map. Why?

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.

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

7 of 28 references.

References · 7

  1. 2023GPT-4 Technical Reportcited by 18,396
  2. 2022Autoformalization with Large Language Modelscited by 263
  3. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  4. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  5. 2023Multilingual Mathematical Autoformalizationcited by 39
  6. 2019Formalising perfectoid spacescited by 7
  7. 2022Formalising the h-principle and sphere eversioncited by 6

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 2; 2025: 5; 2026: 2.

9 papers.

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  2. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 21
  3. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 21
  4. 2024Customize Segment Anything Model for Multi-Modal Semantic Segmentation with Mixture of LoRA Expertscited by 15
  5. 2025Automated Formalization via Conceptual Retrieval-Augmented LLMscited by 5
  6. 2025KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignmentcited by 1
  7. 2025TopoAlign: A Framework for Aligning Code to Math via Topological Decompositioncited by 0
  8. 2026Symbolic Informalization: Fluent, Productive, Multilingualcited by 0
  9. 2026Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematicscited by 0