GFLean: An Autoformalisation Framework for Lean via GF
Shashank Pathak
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.