GFLean: An Autoformalisation Framework for Lean via GF
This work addresses autoformalisation for theorem proving, but it appears incremental as it builds on existing tools and discusses limitations without presenting concrete performance gains.
The authors tackled the problem of autoformalisation for the Lean theorem prover by developing GFLean, a framework that uses Grammatical Framework for parsing and linearisation, implemented in Haskell, and they explored combining neural and rule-based translation methods to enhance robustness.
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.