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 an…