Abstracts.2021.ProofGrammar

On the Grammar of Proof

by Warrick Macmillan

Abstract

The notion of proof in mathematics has manifold interpretations: with the distinction between formal and informal proofs representing a significant spectrum from which to develop and discuss them. One mechanism of understanding this degree of formality is via translation between natural language proofs and those one writes via a proof assistant. Grammatical Framework (GF), a domain-specific functional programming language for specifying grammars which allows for translation by composing a parser and a pretty printer (or linearizer), can be used to translate informal and formal proofs. We contrast how different grammars in GF can be utilized for this task of proof translation, and see how these grammars enable the possibility of both natural language generation and autoformalization, but also offer intractable problems at scale.

Resources

Warrick's thesis

Video Recording