In this chapter I will provide a variety of background material that will be used in later chapters. Later chapters will include links to the relevant sections of this chapter. I cover a variety of topics:

Section 2.1 gives an overview of how proof assistants are designed. This provides some context to place this thesis within the field of ITP.

Section 2.2 contains some preliminary definitions and notation for types, terms, datatypes and functors that will be used throughout the document.

Section 2.3 contains some additional features of inductive datatypes that I will make use of in various places throughout the text.

Section 2.4 discusses the way in which metavariables and tactics work within the Lean theorem prover, the system in which the software I write is implemented.

Section 2.5 switches gears and surveys the existing work in the field of user interfaces for theorem provers. This is background to Chapter 5.

Section 2.6 asks what it means for a person to understand or be confident in a proof. This is used to motivate the work in Chapter 3 and Chapter 4. It is also used to frame the user study I present in Chapter 6.

Section 2.7 explores what the automated reasoning literature has to say on how to define and make use of 'human-like reasoning'. This includes a survey of proof planning (Section 2.7.2).

Section 2.8 surveys the topic of natural language generation of mathematical texts, used in Section 3.6.

# 2.1. The architecture of proof assistants, briefly

In this section I am going to provide an overview of the designs of proof assistants for non-specialist.
You may safely skip this section if you are already familiar with them.
The structure of this section is inspired by the viewpoint that Andrej Bauer expresses in a MathOverflow answer [Bau20[Bau20]Bauer, Andrej*What makes dependent type theory more suitable than set theory for proof assistants?* (2020)].

A typical architecture of a modern, full-fledged checker-style proof assistant is given in Figure 2.1.

The essential purpose of a proof assistant is to represent mathematical theorems, definitions and proofs in a language that can be robustly checked by a computer. This language is called the **foundation language** equipped with a set of **derivation rules**. The language defines the set of objects that formally represPbibent mathematical statements and proofs, and the inference rules and axioms provide the valid ways in which these objects can be manipulatedAt this point, we may raise a number of philosophical objections such as whether the structures and derivations 'really' represent mathematical reasoning.
The curious reader may enjoy the account given in the first chapter of *Logic for Mathematicians* by J. Barkley Rosser [Ros53].[Ros53]Rosser, J. Barkley*Logic for Mathematicians* (1953).
Some examples of foundations are first-order logic (FOL)https://en.wikipedia.org/wiki/First-order_logic, higher-order logic (HOL)https://en.wikipedia.org/wiki/Higher-order_logic, and various forms of dependent type theory (DTT) [Mar84[Mar84]Martin-Löf, Per*Intuitionistic type theory* (1984), CH88[CH88]Coquand, Thierry; Huet, Gérard P.*The Calculus of Constructions* (1988)Inf. Comput., PP89[PP89]Pfenning, Frank; Paulin-Mohring, Christine*Inductively defined types in the Calculus of Constructions* (1989)International Conference on Mathematical Foundations of Programming Semantics, Pro13[Pro13]The Univalent Foundations Program*Homotopy Type Theory: Univalent Foundations of Mathematics* (2013)].

A component of the software called the **kernel** checks proofs in the foundation.
There are numerous foundations and kernel designs.
Finding new foundations for mathematics is an open research area but FOL, HOL and DTT mentioned above are the most well-established for performing mathematics.
I will categorise kernels as being either 'checkers' or 'builders'.

A 'checker' kernel takes as input a proof expression and outputs a yes/no answer to whether the term is a valid proof.
An example of this is the Lean 3 kernel [MKA+15[MKA+15]de Moura, Leonardo; Kong, Soonho; *et al.**The Lean theorem prover (system description)* (2015)International Conference on Automated Deduction].

A 'builder' kernel provides a fixed set of partial functions that can be used to build proofs.
Anything that this set of functions accepts is considered as valid.
This is called an LCF architecture, originating with Milner [Mil72[Mil72]Milner, Robin*Logic for computable functions description of a machine implementation* (1972), Gor00[Gor00]Gordon, Mike*From LCF to HOL: a short history* (2000)Proof, language, and interaction]. The most widely used 'builder' is the Isabelle kernel by Paulson [Pau89[Pau89]Paulson, Lawrence C*The foundation of a generic theorem prover* (1989)Journal of Automated Reasoning].

Most kernels stick to a single foundation or family of foundations. The exception is Isabelle, which instead provides a 'meta-foundation' for defining foundations, however the majority of work in Isabelle uses the HOL foundation.

## 2.1.1. The need for a vernacular

One typically wants the kernel to be as simple as possible, because any bugs in the kernel may result in 'proving' a false statement. For the same reason, the foundation language should also be as simple as possible. However there is a trade-off between kernel simplicity and the usability and readability of the foundation language: if the machine-verified definitions and lemmas are tedious to read and write then the prover will not be adopted by users.

Proof assistant designers need to bridge this gap between a human-readable, human-understandable proof and a machine-readable, machine-checkable proof.
A common approach is to use a second language called the **vernacular** (shown on Figure 2.1).
The vernacular is designed as a human-and-machine-readable compromise that is converted to the foundation language through a process called **elaboration** (e.g., [MAKR15[MAKR15]de Moura, Leonardo; Avigad, Jeremy; *et al.**Elaboration in Dependent Type Theory* (2015)CoRR]).
The vernacular typically includes a variety of essential features such as implicit arguments and some form of type inference, as well as high-level programming features such as pattern matching.
Optionally, there may be a compiler (see Figure 2.1) for the vernacular to also produce runnable code, for example Lean 3 can compile vernacular to bytecode [EUR+17[EUR+17]Ebner, Gabriel; Ullrich, Sebastian; *et al.**A metaprogramming framework for formal verification* (2017)Proceedings of the ACM on Programming Languages].

I discuss some work on provers with the vernacular being a restricted form of natural language as one might find in a textbook in Section 2.8.2.

## 2.1.2. Programs for proving

Using this kernel for checking proofs and a vernacular structure for expressing theorems, we now need to be able to construct proofs of these theorems.

An **Automated Theorem Prover** (ATP) is a piece of software that produces proofs for a formal theorem statement automatically with a minimal amount of user input as to how to solve the proof, examples include Z3https://github.com/Z3Prover/z3, Ehttps://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html and Vampirehttp://www.vprover.org/.

**Interactive Theorem Proving** (ITP) is the process of creating proofs incrementally through user interaction with a prover.
I will provide a review of user interfaces for ITP in Section 2.5.
Most proof assistants incorporate various automated and interactive theorem proving components.

A common modality for allowing the user to interactively construct proofs is with the **proof script** (Figure 2.2), this is a sequence of textual commands, written by the user to invoke certain proving programs called **tactics** that manipulate a state representing a partially constructed proof.
Some of these tactics my invoke various ATPs to assist in constructing proofs.
Proof scripts may be purely linear as in Figure 2.2 or have a hierarchical structure such as in Isar [Wen99[Wen99]Wenzel, Makarius*Isar-a generic interpretative approach to readable formal proof documents* (1999)TPHOLs] or HiProof [ADL10[ADL10]Aspinall, David; Denney, Ewen; *et al.**Tactics for hierarchical proof* (2010)Mathematics in Computer Science].

An alternative to a proof script is for the prover to generate an auxillary proof object file that holds a representation of the proof that is not intended to be human readable.
This is the approach taken by PVS [SORS01[SORS01]Shankar, Natarajan; Owre, Sam; *et al.**PVS prover guide* (2001)Computer Science Laboratory, SRI International, Menlo Park, CA] although I will not investigate this approach further in this thesis.

In the process of proving a statement, a prover must keep track of partially built proofs.
I will refer to these representations of partially built proofs as **development calculi**. I will return to development calculi in Section 2.4.

## 2.1.3. Foundation

A **foundation** for a prover is built from the following pieces:

A

**language**: defining inductive trees of data that we wish to talk about and also syntax for these trees.The

**judgements**: meta-level predicates over the above trees.The

**derivation rules**: a generative set of rules for deriving judgements from other judgements.

To illustrate briefly, the language of simply typed lambda calculus would be expressed as in (2.3).

In (2.3), the purple greek and italicised letters (`𝑥`

, `𝑦`

, `α`

, ...) here are called **nonterminals**.
They say: "You can replace me with any of the items on the right-hand-side of my `::=`

".
So, for example, "`α`

" can be replaced with either a member of `A`

or "`α → β`

".
The words in the final column give a natural language noun to describe the 'type' of the syntax.

In general terms, **contexts** `Γ`

perform the role of tracking which variables are currently in scope.
To see why contexts are needed, consider the expression `𝑥 + 𝑦`

; its resulting type depends on the types of the variables `𝑥`

and `𝑦`

.
If `𝑥`

and `𝑦`

are both natural numbers, `𝑥 + 𝑦`

will be a natural number and similarly for integers or complex numbers.
The correct interpretation of `𝑥 + 𝑦`

depends on the *context* of the expression.

Next we define the judgements for our system in (2.4).

Then write down the **natural deduction** rules (2.5) for inductively deriving these judgements.

And from this point, it is possible to start exploring the ramifications of the system. For example: is `Γ ⊢ 𝑠 : α`

decidable?

Every proof assistant worth its salt needs to define the foundation in this way.
These are usually written down in papers as a BNF grammar and a spread of gammas, turnstiles and lines as illustrated in (2.3), (2.4) and (2.5).
Or as Steele calls it: Computer Science Metanotation [Ste17[Ste17]Steele Jr., Guy L.*It's Time for a New Old Language* (2017)].

In *implementations* of proof assistants, the foundation typically doesn't separate quite as cleanly in to the above pieces.
The language is implemented with a number of optimisations such as de Bruijn indexing [deB72[deB72]de Bruijn, Nicolaas Govert*Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem* (1972)Indagationes Mathematicae (Proceedings)] for the sake of efficiency.
Judgements and rules are implicitly encoded in algorithms such as type checking, or appear in forms different from that in the corresponding paper.

In this thesis I will be using the Martin-Löf-style [Mar84[Mar84]Martin-Löf, Per*Intuitionistic type theory* (1984)] dependent type theory of Lean 3 as implemented by de Moura *et al* and formally documented by Carneiro [Car19[Car19]Carneiro, Mario*Lean's Type Theory* (2019)].
A good introduction to mathematical formalisation with dependent type theory is the first chapter of the *HoTT Book* [Pro13[Pro13]The Univalent Foundations Program*Homotopy Type Theory: Univalent Foundations of Mathematics* (2013) ch. 1].
Other foundations are also available: Isabelle's foundation is two-tiered [Pau89[Pau89]Paulson, Lawrence C*The foundation of a generic theorem prover* (1989)Journal of Automated Reasoning]: there is a meta-level foundation upon which many foundations can be implemented. A lot of the work in this thesis is independent of foundation and so I will try to indicate where I can how the contributions can be augmented to work in other foundations.

# 2.2. Preliminaries

This section contains a set of quick preliminary definitions for the concepts and notation that I will be using later. In this thesis I will be using a typed pseudolanguage which should be familiar to most functional programming enthusiasts. This pseudo-language is purely presentational; it will be abused in the name of clarity. If you are comfortable with functional programming and dependent type theory feel free to skip to Section 2.3.

## 2.2.1. Some notation for talking about type theory and algorithms

You can skip over this section if you are comfortable with dependently-typed functional programming.

The world is built of **types** and **terms**.
New variables are introduced as "`𝑥 : A`

"; `𝑥`

is the variable and it has the type `A`

.
Lots of variables with the same type can be introduced as `𝑥 𝑦 𝑧 : A`

.
Types `A B C : Type`

start with an uppercase letter and are coloured turquoise. `Type`

is a special 'type of types'Of course, since this is just pseudocode, we do not have to worry about paradoxes as when choosing a prover foundation in Section 2.4.1..
Meanwhile terms start with a lowercase letter and term variables are purple and italicised.
`A → B`

is the function type. `→`

is *right associative* which means that `𝑓 : A → B → C`

should be read as `𝑓 : A → (B → C)`

.
This is called a **curried function**, we may consider `A`

and `B`

to be the input arguments of `𝑓`

and `C`

to be its return type.
Given `𝑎 : A`

we may *apply* `𝑓`

to `𝑎`

by writing `𝑓 𝑎 : B → C`

.
Functions are introduced using maps-to notation `(𝑎 : A) ↦ (𝑏 : B) ↦ 𝑓 𝑎 𝑏`

.
Write the identity function `𝑥 ↦ 𝑥`

as `𝟙 : X → X`

. Given `𝑓 : A → B`

, `𝑔 : B → C`

, write function composition as `𝑔 ∘ 𝑓 : A → C`

.
Function application is left associative, so `𝑓 𝑎 𝑏`

should be read as `(𝑓(𝑎))(𝑏)`

.
The input types of functions may be optionally be given argument names, such as: `(𝑎 : A) → (𝑏 : B) → C`

. We also allow 'dependent types' where the return value `C`

is allowed to depend on these arguments: `(𝑎 : A) → 𝒞 𝑎`

where `𝒞 : A → Type`

is a **type-valued function**.

`Empty`

is the empty type.`Unit`

is the type containing a single element`()`

.`Bool`

is the boolean type ranging over values`true`

and`false`

.`Option X`

or`X?`

is the type taking values`some 𝑥`

for`𝑥 : X`

or`none`

.`some`

will usually be suppressed.`List X`

or`X*`

is the type of finite lists of`X`

. Given`𝑥 𝑦 : X`

and`𝑙₁ 𝑙₂ : List X`

, we can write`𝑥 :: 𝑙₁`

for list cons and`𝑙₁ ++ 𝑙₂`

for concatenating two lists. For list construction and pattern matching, list*spreads*will be used. For example`[..𝑙₁, 𝑥, 𝑦, ..𝑙₂]`

denotes the list formed by concatenating`𝑙₁`

,`[𝑥, 𝑦]`

and`𝑙₂`

. Python-style list comprehensions are also used:`[𝑖² for 𝑖 in 1..20]`

is a list of the first 20 square numbers.`ℕ`

is the type of natural numbers. Individual numbers can be used as types:`𝑥 : 3`

means that`𝑥`

is a natural number taking any value`𝑥 < 3`

, i.e,`𝑥 ∈ {0,1,2}`

.`A × B`

is the type of tupleshttps://en.wikipedia.org/wiki/Tuple over`A`

and`B`

. Elements are written as`(a, b) : A × B`

. As usual we have projections`π₁ (𝑎, 𝑏) := 𝑎`

and`π₂ (𝑎, 𝑏) := 𝑏`

. Members of tuples may be given names as`(a : A) × (b : B)`

. In this case, supposing`p : (a : A) × (b : B)`

, we can write`p.a`

and`p.b`

instead of`π₁ p`

and`π₂ p`

. Similarly to above, we can have a dependent tuple or 'sigma type'`(a : A) × (b : B(a))`

.`A + B`

is the discriminated union of`A`

and`B`

with constructors`inl : A → A + B`

and`inr : B → A + B`

.

## 2.2.2. Functors and monads

I will assume that the readers are already familiar with the motivation behind functors and monads in category theory and as used in e.g. Haskell but I will summarise them here for completeness.
I refer the unfamiliar reader to the Haskell *Typeclassopedia*https://wiki.haskell.org/Typeclassopedia.

Here, a **functor** will mean a type-valued function `F : Type → Type`

equipped with a function mapper `F (𝑓 : A → B) : F A → F B`

So here, the word 'functor' is used to mean the special case of category-theoretical endofunctors on the category of `Type`

s and functions between them.. I will here always assume that the functor is **lawful**, which here means it obeys the functor laws (2.6).

A **natural function** `a : F ⇒ G`

between functors `F G : Type → Type`

is a family of functions `a[A] : F A → G A`

indexed by `A : Type`

such that `a[B] ∘ F f = G f ∘ a[A]`

for all `f : A → B`

. Often the type argument to `a`

will be suppressed.
It is quick to verify that the functors and natural functors over them form a category.

A **monad**For learning about programming with monads, I recommend https://wiki.haskell.org/All_About_Monads. `M : Type → Type`

is a functor equipped with two natural functions `pure : 𝟙 ⇒ M`

and `join : M M ⇒ M`

obeying the monad laws (2.7). Write `𝑚 >>= 𝑓 := join (M 𝑓 𝑚)`

for `𝑚 : M A`

and `𝑓 : A → M B`

.
`do`

notationhttps://wiki.haskell.org/Keywords#do will be used in places.

An **applicative functor** [MP08[MP08]McBride, Conor; Paterson, Ross*Applicative programming with effects* (2008)J. Funct. Program. §2] `M : Type → Type`

is equipped with `pure : A → M A`

and `seq : M (A → B) → M A → M B`

.
Write `𝑓 <*> 𝑎 := seq 𝑓 𝑥`

`<*>`

is left associative: `𝑢 <*> 𝑣 <*> 𝑤 = (𝑢 <*> 𝑣) <*> 𝑤`

. and `𝑎 *> 𝑏 := seq (_ ↦ 𝑎) 𝑏`

. Applicative functors obey the laws given in (2.8).

## 2.2.3. Inductive datatypes

New inductive datatypes are defined with a GADT-like syntaxhttps://wiki.haskell.org/Generalised_algebraic_datatype (2.9).

In cases where it is obvious which constructor is being used the tag names will be suppressed. Function definitions with pattern matching will use the syntax given in (2.10).

One can express inductive datatypes `D`

as fixpoints of functors `D = Fix P`

where `Fix P := P (Fix P)`

.
Depending on the underlying category, `Fix P`

will not exist for all `P`

Smyth and Plotkin are the first to place some conditions on when the fixpoint exists [SP82], see Adámek *et al* for a survey [AMM18].[SP82]Smyth, Michael B; Plotkin, Gordon D*The category-theoretic solution of recursive domain equations* (1982)SIAM Journal on Computing, [AMM18]Adámek, Jiří; Milius, Stefan; *et al.**Fixed points of functors* (2018)J. Log. Algebraic Methods Program..

When a `D : Type`

may be written as `Fix P`

for some `P`

Strictly, we should also include an irreducibility condition: there is no `Q`

such that `P = Q ∘ Q ∘ ... ∘ Q`

., `P`

will be called the **base functor**https://hackage.haskell.org/package/recursion-schemes-5.2.2/docs/Data-Functor-Base.html for `D`

.
This conceptualisation is useful because we can use the base functor to make related types without needing to explicitly write down the constructors for the modified versions. For example we could make the list lazy with `Lazy P X := Fix ((X ↦ Unit → X) ∘ P)`

.

# 2.3. Inductive gadgets

For the rest of this thesis, I will make use of a few motifs for discussing inductive datastructures, particularly in Section 2.4, Chapter 3, Appendix A and Appendix C. In this section I will lay some background material for working with inductive datatypes. This is covered in various forms in the literature and within implementations of functional programming languages such as Haskellhttps://www.haskell.org/, although the presentation here differs from how I have seen it elsewhere. A framing of inductive datatypes that I have found very helpful but which I have not found an account of in the literature are the concept of 'coordinates' for datatypes (Section 2.3.2).

## 2.3.1. Traversable functors

Given a monad `M`

, a common task is performing a monad-map with `f : A → M B`

over a list of objects `l : List X`

.
This is done with the help of a function called `mmap`

(2.11).

But we can generalise `List`

to some functor `T`

; when can we equip an analogous `mmap`

to `T`

?
For example, in the case of binary trees (2.12).

A functor `T : Type → Type`

is **traversable**https://wiki.haskell.org/Typeclassopedia#Traversable when for all applicative functors (Section 2.2.2) `M : Type → Type`

,
there is a natural map `d[M] : (T ∘ M) ⇒ (M ∘ T)`

.
That is, for each `X : Type`

we have `d[M][X] : T (M X) → M (T X)`

.
In addition to being natural, `d`

must obey the traversal laws given in (2.13) [JR12[JR12]Jaskelioff, Mauro; Rypacek, Ondrej*An Investigation of the Laws of Traversals* (2012)Proceedings Fourth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2012, Tallinn, Estonia Definition 3.3].

Given a traversable functor `T`

and a monad `M`

, we can recover `mmap : (A → M B) → T A → M (T B)`

as `mmap 𝑓 𝑡 := d[M][B] (T 𝑓 𝑡)`

.

## 2.3.2. Functors with coordinates

Bird *et al* [BGM+13[BGM+13]Bird, Richard; Gibbons, Jeremy; *et al.**Understanding idiomatic traversals backwards and forwards* (2013)Proceedings of the 2013 ACM SIGPLAN symposium on Haskell] prove that (in the category of sets) the traversable functors are equivalent to a class of functors called finitary containers.
Their theorem states that there is a type `Shape T 𝑛 : Type`

An explicit definition of `Shape T 𝑛`

is the pullback of `children[1] : T Unit ⟶ List Unit`

and `!𝑛 : Unit ⟶ List Unit`

, the list with `𝑛`

elements. for each traversable `T`

and `𝑛 : ℕ`

such that that each `𝑡 : T X`

is isomorphic an object called a **finitary container** on `Shape T`

shown in (2.14).

`map`

and `traverse`

may be defined for the finitary container as `map`

and `traverse`

over the `children`

vector.
Since `𝑡 : T X`

has `𝑡.length`

child elements, they can be indexed by the numbers `{𝑘 : ℕ | 𝑘 < length}`

.
We can then define operations to get and set individual elements according to this index `𝑘`

.

Usually, however, this numerical indexing of the children of `𝑡 : T X`

loses the semantics of the datatype.
As an example; consider the case of a binary tree `Tree`

in (2.15). A tree `𝑡 : Tree X`

with `𝑛`

`branch`

components will have length `𝑛`

and a corresponding `children : Vec 𝑛 X`

, but indexing via numerical indices `{𝑘 | 𝑘 < 𝑛}`

loses information about where the particular child `𝑥 : X`

can be found in the tree.

Now I will introduce a new way of indexing the members of children for the purpose of reasoning about inductive datatypes.
This idea has been used and noted before many times, the main one being the idea of *paths* in universal algebra [BN98[BN98]Baader, Franz; Nipkow, Tobias*Term rewriting and all that* (1998) Dfn. 3.1.3].
However I have not seen an explicit account of this idea in the general setting of traversable functors and later in Section 2.3.3 to general inductive datatypes.

A traversable functor `T`

**has coordinates** when equipped with a type `C : Type`

and a function `coords[𝑛] : Shape T 𝑛 → Vec 𝑛 C`

.
The `coords`

function amounts to a labelling of the `𝑛`

children of a particular shape with members of `C`

.

Often when using traversals, working with the children list `Vec (length 𝑡) X`

for each shape of `T`

can become unwieldy, it is convenient to instead explicitly provide a pair of functions `get`

and `set`

(2.16) for manipulating particular children of a given `𝑡 : T X`

.

`C`

is not unique, and in general should be chosen to have some semantic value for thinking about the structure of `T`

.
Here are some examples of functors with coordinates:

`List`

has coordinates`ℕ`

.`coords 𝑙`

for`𝑙 : List X`

returns a list`[0, ⋯, 𝑙.length - 1]`

.`get 𝑖 𝑙`

is`some 𝑙[𝑖]`

and`set 𝑖 𝑙 𝑥`

returns a new list with the`𝑖`

th element set to be`𝑥`

.`Vec n`

, lists of length`n`

, has coordinates`{k : ℕ | k < n}`

with the same methods as for`List`

above.`Option`

has coordinates`Unit`

.`coords (some 𝑥) := [()]`

and`coords none := []`

.`get _ 𝑜 := 𝑜`

and`set`

replaces the value of the option.Binary trees have coordinates

`List D`

as shown in (2.17).

## 2.3.3. Coordinates on initial algebras of traversable functors

Given a functor `F`

with coordinates `C`

, we can induce coordinates on the free monad `Free F : Type → Type`

of `F`

.
The free monad is defined concretely in (2.18).

We can write `Free F X`

as the fixpoint of `A ↦ X + F A`

As mentioned in Section 2.2.3, these fixpoints may not exist, but I will assume that they do here for the `F`

s of concern..
`Free F`

has coordinates `List C`

with methods defined in (2.19).

In a similar manner, `List C`

can be used to reference particular subtrees of an inductive datatype `D`

which is the fixpoint of a traversable functor `D = F D`

.
Let `F`

have coordinates `C`

.
`D`

here is not a functor, but we can similarly define `coords : D → List (List C)`

, `get : List C → Option D`

and `set : List C → D → D → D`

.

The advantage of using coordinates over some other system such as opticshttp://hackage.haskell.org/package/lens [FGM+07[FGM+07]Foster, J Nathan; Greenwald, Michael B; *et al.**Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem* (2007)ACM Transactions on Programming Languages and Systems (TOPLAS)] or other apparati for working with datatypes [LP03[LP03]Lämmel, Ralf; Peyton Jones, Simon*Scrap Your Boilerplate* (2003)Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedings] is that they are much simpler to reason about.
A coordinate is just an address of a particular subtree.
Another advantage is that the choice of `C`

can convey some semantics on what the coordinate is referencing (for example, `C = left | right`

in (2.17)), which can be lost in other ways of manipulating datastructures.

# 2.4. Metavariables

Now with a way of talking about logical foundations, we can resume from Section 2.1.2 and consider the problem of how to represent partially constructed terms and proofs given a foundation.
This is the purpose of a **development calculus**: to take some logical system $L$ and produce some new system $DL$ such that one can incrementally build terms and proofs in a way that provides feedback at intermediate points and ensures that various judgements hold for these intermediate terms.
In Chapter 3, I will create a new development calculus for building human-like proofs, and in Appendix A this system will be connected to Lean. we need to first look at how Lean's current development calculus behaves.
Since I will be using Lean 3 in this thesis and performing various operations over its expressions, I will follow the same general setup as is used in Lean 3.
The design presented here was first developed by Spiwack [Spi11[Spi11]Spiwack, Arnaud*Verified computing in homological algebra, a journey exploring the power and limits of dependent type theory* (2011)] first released in Coq 8.5.
It was built to allow for a type-safe treatment of creating tactics with metavariables in a dependently-typed foundation.

## 2.4.1. Expressions and types

In this section I will introduce the expression foundation language that will be used for the remainder of the thesis. The system presented here is typical of expression structures found in DTT-based provers such as Lean 3 and Coq. I will not go in to detail on induction schema and other advanced features because the work in this thesis is independent of them.

Here, `Level`

can be thought of as expressions over some signature that evaluate to natural numbers, they are used to stratify Lean's types so that one can avoid Girard's paradox [Hur95[Hur95]Hurkens, Antonius JC*A simplification of Girard's paradox* (1995)International Conference on Typed Lambda Calculi and Applications].
`Name`

is just a type of easily distinguishable identifiers, in the case of Lean they are lists of strings or numbers.
Sugar `lambda 𝑥 α 𝑏`

as `λ (𝑥 ∶ α), 𝑏`

, `pi 𝑥 α 𝑏`

as `Π (𝑥 ∶ α), 𝑏`

, `app 𝑓 𝑎`

as `𝑓 𝑎`

and omit `var`

and `const`

when it is clear what the appropriate constructor is.

Using `ExprBase`

, we may define pure expressions `Expr := Fix ExprBase`

as in Section 2.2.3.
Note that it is important to distinguish between the meta-level type system introduced in Section 2.2 and the object-level type system where the 'types' are merely instances of `Expr`

To help with this distinction, I have made an effort to annotated any object-level type assignment statements such as `(𝑥 ∶ α)`

with a variant of the colon `∶`

as opposed to `:`

..

Variables may be **bound** by `λ`

and `Π`

expressions. For example, in `λ (𝑥 ∶ α), 𝑡`

, we say that the expression **binds** `𝑥`

in `𝑡`

.
If `𝑡`

contains variables that are not bound, these are called **free** variables.
Now given a partial map `σ : Name ⇀ Expr`

and a term `𝑡 : Expr`

, define a **substitution** `subst σ 𝑡 : Expr`

as in (2.21).
This will be written as `σ 𝑡`

for brevity.

I will denote substitutions as a list of `Name ↦ Expr`

pairs. For example `⦃𝑥 ↦ 𝑡, 𝑦 ↦ 𝑠⦄`

where `𝑥 𝑦 : Name`

are the variables which will be substituted for terms `𝑡 𝑠 : Expr`

respectively.

Substitution can easily lead to badly-formed expressions if there are variable naming clashes.
I need only note here that we can always perform a renaming of variables in a given expression to avoid clashes upon substitution.
These clashes are usually avoided within prover implementations with the help of de-Bruijn indexing [deB72[deB72]de Bruijn, Nicolaas Govert*Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem* (1972)Indagationes Mathematicae (Proceedings)].

## 2.4.2. Assignable datatypes

Given an expression structure `Expr`

and `𝑡 : Expr`

, we can define a traversal over all of the immediate subexpressions of `𝑡`

.
However, in order to perform variable-oriented operations such as abstraction and substitution, we need to take care when traversing a subexpression that lies under a binder.
For example for lambda binders `𝑡 = λ (𝑥 : α), 𝑏`

, the subexpression `𝑡`

has a free variable `𝑥`

.

Once you have this child-traversal function, one can derive all of one's favourite context-aware expression manipulating tools:

The idea here is to generalise `child_traverse`

to include any datatype that may involve expressions.
Frequently when building systems for proving, one has to make custom datastructures. For example one might wish to create a 'rewrite-rule' structure for modelling equational reasoning (as will be done in Chapter 4):

But now if we want to perform a variable instantiation or count the number of free variables present in `𝑟 : RewriteRule`

, we have to write custom definitions to do this.
The usual traversal functions from Section 2.3.1 are not adequate here, because we may need to take in to account a binder structure. For example traversing `Context`

as a simple list of names and expressions will produce the wrong output for `fv`

, because some of the variables are bound by previous binders in the context.

To avoid having to write all of this boilerplate, let's make a typeclass `assignable`

(2.25) on datatypes that we need to manipulate the expressions in.
Say that

Now, provided `expr_traverse`

is defined for `X`

, `fv`

, `instantiate`

and other expression-manipulating operations such as those in (2.23) can be modified to use `expr_traverse`

instead of `child_traverse`

.
This `assignable`

regime becomes very useful using de-Bruijn indices to represent bound variables [deB72[deB72]de Bruijn, Nicolaas Govert*Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem* (1972)Indagationes Mathematicae (Proceedings)] because the length of `Γ`

can be used to determine the binder depth of the current expression.
An example implementation including many more examples of implementations of `assignable`

and expression-manipulating operations that can make use of `assignable`

can be found in the my Lean implementation of this concepthttps://github.com/leanprover-community/mathlib/pull/5719.

## 2.4.3. Lean's development calculus

In the Lean source code, there are other constructors for `Expr`

other than those in (2.21).
Some are for convenience or efficiency reasons (such as Lean 3 macros), but others are part of the Lean development calculus.
The main development calculus construction is `mvar`

or a **metavariable**, sometimes also called **existential variables** or **schematic variables**.
An mvar `?m`

acts as a 'hole' for an expression to be placed in later.
There is no kernel machinery to guarantee that an expression containing a metavariable is correct, instead they are used for the process of building expressions.

As an example, suppose that we needed to prove `P ∧ Q`

for some propositions `P Q ∶ Prop`

.
The metavariable-based approach to proving this would be to **declare** a new metavariable `?𝑡 : P ∧ Q`

.
Then, a program might try to solve this metavariable in two steps; declare two new metavariables `?𝑡₁ : P`

and `?𝑡₂ : Q`

; and then **assign** `?𝑡`

with the expression `and.make ?𝑡₁ ?𝑡₂`

where `and.make : P → Q → P ∧ Q`

creates 'and' proofs.
After this, `?𝑡₁`

and `?𝑡₂`

may themselves be assigned with `p : P`

and `q : Q`

.
In this way, the proof term can be built up slowly as `?𝑡 ⟿ and.make ?𝑡₁ ?𝑡₂ ⟿ and.make p ?𝑡₂ ⟿ and.make p q`

.
This process is much more convenient for building modular programs that construct proofs than requiring that a pure proof term be made all in one go.

Lean comes with a development calculus that uses metavariables.
This section can be viewed as a more detailed version of the account originally given by de Moura *et al* [MAKR15[MAKR15]de Moura, Leonardo; Avigad, Jeremy; *et al.**Elaboration in Dependent Type Theory* (2015)CoRR §3.2] with the additional details sourced from inspecting the Lean source codehttps://github.com/leanprover-community/lean.
The first use of this kind of development calculus was in of Spiwack's thesis [Spi11], where the tactic monad for Coq was augmented with a stateful global metavariable context.

The implementation of Lean allows another constructor for `Expr`

to allow for metavariables:

Metavariables are 'expression holes' and are denoted as `?𝑥`

where `𝑥 : Name`

.
They are placeholders into which we promise to substitute a valid pure expression later.
Similarly to `fv(𝑡)`

being the free variables in `𝑡 : Expr`

, we can define `mv(𝑡)`

to be the set of metavariables present in `𝑡`

.
However we still need to be able to typecheck and reduce expressions involving metavariables and so we need to have some additional structure on the context.

The idea is that in addition to a local context `Γ`

, expressions are inspected and created within the scope of a second context called the **metavariable context** `𝑀 : MvarContext`

.
The metavariable context is a dictionary `MvarContext := Name ⇀ MvarDecl`

where each metavariable declaration `𝑑 : MvarDecl`

has the following information:

`identifier : Name`

A unique identifier for the metavariable.`type : Expr`

The type of the metavariable.`context : Context`

The local context of the metavariable. This determines the set of local variables that the metavariable is allowed to depend on.`assignment : Option Expr`

An optional assignment expression. If`assignment`

is not`none`

, say that the metavariable is**assigned**.

The metavariable context can be used to typecheck an expression containing metavariables by assigning each occurrence `?𝑥`

with the type given by the corresponding declaration `𝑀[𝑥].type`

in `𝑀`

.
The `assignment`

field of `MvarDecl`

is used to perform instantiation. We can interpret `𝑀`

as a substitution.

As mentioned in Section 2.1.2, the purpose of the development calculus is to represent a partially constructed proof or term. The kernel does not need to check expressions in the development calculus (which here means expressions containing metavariables), so there is no need to ensure that an expression using metavariables is sound in the sense of Section 2.1.3 for some set of inference rules such as those given in (2.5). However, in Section A.1, I will provide some inference rules for typing expressions containing metavariables to assist in showing that the system introduced in Chapter 3 is compatible with Lean.

## 2.4.4. Tactics

A partially constructed proof or term in Lean is represented as a `TacticState`

object.
For our purposes, this can be considered as holding the following data:

The `result`

field is the final expression that will be returned when the tactic completes.
`goals`

is a list of metavariables that are used to denote what the tactic state is currently 'focussing on'.
Both `goals`

and `result`

are in the context of `mctx`

.

`Tactic`

s may perform actions such as modifying the `goals`

or performing assignments of metavariables.
In this way, a user may interactively build a proof object by issuing a stream of tactics.

# 2.5. User interfaces for provers

Now let's talk about something completely different: user interfaces. One research question in Section 1.2 is to investigate how human-like reasoning can be enabled through the use of interactive graphical user interfaces (GUIs). The field of ITP has a rich history of using rich graphical user interfaces to represent and interact with proofs and expressions. Here I will provide a brief review of these. The background covered in this section will then be picked up for Chapter 5, where I introduce my own GUI framework for ITP.

An early general user interface for interactive proving was Aspinall's *Proof General* [Asp00[Asp00]Aspinall, David*Proof General: A generic tool for proof development* (2000)International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ALW07[ALW07]Aspinall, David; Lüth, Christoph; *et al.**A framework for interactive proof* (2007)Towards Mechanized Mathematical Assistants]. This took the form of an Emacshttps://www.gnu.org/software/emacs/ extension that offered a general purpose APIApplication programming interface. A set of protocols to allow two applications to communicate with each other. for controlling proof assistants such as Isabelle. A typical Proof General session would make use of two text buffers: the proof script buffer and the goal state buffer. Users type commands in to the script buffer, and observe changes in the goal state buffer. This two-panel setup remains the predominant workflow for proof assistants today. Proof General also offers the ability to perform interaction with the goal state, for example 'proof-by-pointing' with subexpressions in the output window.

The idea proof-by-pointing will play a key role in Section 5.4. It was first described by Bertot and Théry [BT98[BT98]Bertot, Yves; Théry, Laurent*A generic approach to building user interfaces for theorem provers* (1998)Journal of Symbolic Computation]. The idea of proof-by-pointing is to preserve the semantics of pretty-printedA pretty-printed expression is a string of characters that represents an expression in the underlying foundation of a prover. For example the string `𝑥 + 𝑦`

is the pretty printed form of the expression `app (app (const "plus") (var "𝑥")) (var "𝑦")`

. expressions so that a user may inspect the tree structure of the expression through pointing to different parts of the string.

The most advanced specially-created IDEIntegrated Development Environment for proving is Isabelle's Prover IDE (PIDE) [Wen12[Wen12]Wenzel, Makarius*Isabelle/jEdit-A Prover IDE within the PIDE Framework.* (2012)AISC/MKM/Calculemus], developed primarily by Makarius Wenzel in Scalahttps://www.scala-lang.org/ and based on the JEdit text editorhttp://jedit.org. PIDE richly annotates Isabelle documents and proof states to provide inline documentation; interactive and customisable commands; and automatic insertion of text among other features. PIDE uses a Java GUI library called Swinghttps://docs.oracle.com/javase/8/docs/technotes/guides/swing/. Isabelle's development environment allows users to code their own GUI in Scala.
There have been some recent efforts to support VSCodehttps://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode as a client editor for Isabelle files.
A web-based client for Isabelle, called *Clide* [LR13[LR13]Lüth, Christoph; Ring, Martin*A web interface for Isabelle: The next generation* (2013)International Conference on Intelligent Computer Mathematics] was developed, although it provided only a subset of the functionality of the JEdit version.

SerAPI [Gal16[Gal16]Gallego Arias, Emilio Jesús*SerAPI: Machine-Friendly, Data-Centric Serialization for Coq* (2016)] is a library for machine-machine interaction with the Coq theorem prover.
The project supports some web-based IDE projects such as jsCoq [GPJ17[GPJ17]Gallego Arias, Emilio Jesús; Pin, Benoît; *et al.**jsCoq: Towards Hybrid Theorem Proving Interfaces* (2017)Proceedings of the 12th Workshop on User Interfaces for Theorem Provers] and PeaCoqhttp://goto.ucsd.edu/peacoq/.
Very recently, a framework called Alectyron [Pit20[Pit20]Pit-Claudel, Clément*Untangling mechanized proofs* (2020)SLE 2020: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering] has been released for Coq that enables users to embed web-based representations of data (see the link for more details).

There are some older GUI-centric theorem provers that have fallen out of use: LΩUI [SHB+99[SHB+99]Siekmann, Jörg; Hess, Stephan; *et al.**LOUI: Lovely OMEGA user interface* (1999)Formal Aspects of Computing], HyperProof [BE92[BE92]Barwise, Jon; Etchemendy, John*Hyperproof: Logical reasoning with diagrams* (1992)Working Notes of the AAAI Spring Symposium on Reasoning with Diagrammatic Representations] and XBarnacle [LD97[LD97]Lowe, Helen; Duncan, David*XBarnacle: Making theorem provers more accessible* (1997)Automated Deduction—CADE-14].
These tools were all highly innovative for including graphical and multimodal representations of proofs, however the code for these seems to have been lost, paywalled or succumbed to bit rothttps://en.wikipedia.org/wiki/Software_rot, to the extent that I can only view them through the screenshots that they included with the papers. Source code for Ωmega and CLAM (which LΩUI and XBarnacle use respectively) can be found in the Theorem Prover Museumhttps://theoremprover-museum.github.io/.

Another contemporary proof assistants with specially made GUIs are Theorema [BJK+16[BJK+16]Buchberger, Bruno; Jebelean, Tudor; *et al.**Theorema 2.0: computer-assisted natural-style mathematics* (2016)Journal of Formalized Reasoning] and KeY [ABB+16[ABB+16]Ahrendt, Wolfgang; Beckert, Bernhard; *et al.**Deductive Software Verification - The KeY Book* (2016)].
Theorema is built upon the computer algebra system Wolfram Mathematicahttps://www.wolfram.com/mathematica/ and makes use of its inbuilt @abbr[GUI] framework.
KeY is a theorem prover for verifying Java applications. KeY embraces multimodal views of proofs and offers numerous interactive proof discovery features and interactive proof-by-pointing inspection of subexpressions. In her thesis, Grebing investigates the usability of KeY [Gre19[Gre19]Grebing, Sarah Caecilia*User Interaction in Deductive Interactive Program Verification* (2019)] through the use of focus groups, an approach relevant for my evaluation study in Chapter 6.

Another source of inspiration for me are the theorem prover web-apps: Vicary's *Globular* [VKB18[VKB18]Vicary, Jamie; Kissinger, Aleks; *et al.**Globular: an online proof assistant for higher-dimensional rewriting* (2018)Logical Methods in Computer Science] and Breitner's *Incredible Proof Machine* [Bre16[Bre16]Breitner, Joachim*Visual theorem proving with the Incredible Proof Machine* (2016)International Conference on Interactive Theorem Proving]. These tools are natively web-based and offer a visual representation of the proof state for users to manipulate.

These tools all demonstrate an ongoing commitment by the ITP community to produce graphical user interfaces which explore new ways of respresenting and interacting with proof assistants. It is with these previous works in mind that I design a new kind of general purpose approach to a GUI framework for a prover.

# 2.6. Understandability and confidence

This section is a short survey of literature on what it means for a mathematical proof to be understandable. This is used in Chapter 6 to evaluate my software and to motivate the design of the software in Chapter 3 and Chapter 4. At the end of this section, I hope readers will have gained a sense of what people have already done in this field and to feel that the question is a little less nebulous.

## 2.6.1. Understandability of mathematics in a broader context

What does it mean for a proof to be understandable?
An early answer to this question comes from the 19th century philosopher Spinoza.
Spinoza [Spi87[Spi87]Spinoza, Benedict*The chief works of Benedict de Spinoza* (1887)] supposes 'four levels' of a student's understanding of a given mathematical principle or rule, which are:

**mechanical**: The student has learnt a recipe to solve the problem, but no more than that.**inductive**: The student has verified the correctness of the rule in a few concrete cases.**rational**: The student comprehends a proof of the rule and so can see why it is true generally.**intuitive**: The student is so familiar and immersed in the rule that they cannot comprehend it not being true.

This is a good place to start; for the purposes of this thesis I will restrict my attention to type 3 understanding. That is, how the student digests a proof of a general result. If the student is at level 4, and treats the result like a fish treats water, then there seems to be little an ITP system can offer other than perhaps forcing any surprising counterexamples to arise when the student attempts to formalise it.

Edwina Michener's *Understanding Understanding Mathematics* [Mic78[Mic78]Michener, Edwina Rissland*Understanding understanding mathematics* (1978)Cognitive science] provides a wide ontology of methods for understanding mathematics in a similar fashion to Pólya.
Michener (p. 373) proposes that "understanding is a complementary process to problem solving" and incorporates Spinoza's 4-level model.
She also references Poincaré's thoughts on understanding [Poi14[Poi14]Poincaré, Henri*Science and method* (1914) p. 118], from which I will take an extended quote from the original:

What is understanding? Has the word the same meaning for everybody? Does understanding the demonstration of a theorem consist in examining each of the syllogisms of which it is composed and being convinced that it is correct and conforms to the rules of the game? ...

Yes, for some it is; when they have arrived at the conviction, they will say, I understand. But not for the majority... They want to know not only whether the syllogisms are correct, but why there are linked together in one order rather than in another. As long as they appear to them engendered by caprice, and not by an intelligence constantly conscious of the end to be attained, they do not think they have understood.

In a similar spirit; de Millo, Lipton and Perlis [MUP80[MUP80]de Millo, Richard A; Upton, Richard J; *et al.**Social processes and proofs of theorems and programs* (1980)The mathematical intelligencer] write referring directly to the nascent field of program verification (here referred to 'proofs of software')

Mathematical proofs increase our confidence in the truth of mathematical statements only after they have been subjected to the social mechanisms of the mathematical community. These same mechanisms doom the so-called proofs of software, the long formal verifications that correspond, not to the working mathematical proof, but to the imaginary logical structure that the mathematician conjures up to describe his feeling of belief. Verifications are not messages; a person who ran out into the hall to communicate his latest verification would rapidly find himself a social pariah. Verifications cannot really be read; a reader can flay himself through one of the shorter ones by dint of heroic effort, but that's not reading. Being unreadable and - literally - unspeakable, verifications cannot be internalized, transformed, generalized, used, connected to other disciplines, and eventually incorporated into a community consciousness. They cannot acquire credibility gradually, as a mathematical theorem does; one either believes them blindly, as a pure act of faith, or not at all.

Poincaré's concern is that a verified proof is not sufficient for understanding.
De Millo *et al* question whether a verified proof is a proof at all!
Even if a result has been technically proven, mathematicians care about the structure and ideas behind the proof itself.
If this were not the case, then it would be difficult to explain why new proofs of known results are valued by mathematicians.
The question of what exactly they value is what I wish to explore further in the study in Chapter 6.

Many studies investigating mathematical understanding within an educational context exist, see the work of Sierpinska [Sie90[Sie90]Sierpinska, Anna*Some remarks on understanding in mathematics* (1990)For the learning of mathematics, Sie94[Sie94]Sierpinska, Anna*Understanding in mathematics* (1994)] for a summary. See also Pólya's manual on the same topic [Pól62[Pól62]Pólya, George*Mathematical Discovery* (1962)].

## 2.6.2. Confidence

Another line of inquiry suggested by Poincaré's quote is distinguishing *confidence* in a proof from a proof being *understandable*.
By confidence in a proof, I do not mean confidence in the result being true, but instead confidence in the given script actually being a valid proof of the result.

As an illustrative example, I will give my own impressions on some proofs of the Jordan curve theoremhttps://en.wikipedia.org/wiki/Jordan_curve_theorem which states that any non-intersecting continuous loop in the 2D Euclidean plane has an interior region and an exterior region.
Formal and informal proofs of this theorem are discussed by Hales [Hal07[Hal07]Hales, Thomas C*The Jordan curve theorem, formally and informally* (2007)The American Mathematical Monthly].
I am confident that the proof of the Jordan curve theorem formalised by Hales in the HOL Light proof assistant is correct although I can't claim to understand it in full.
Contrast this with the diagrammatic proof sketch (Figure 2.28) given in Hales' paper (originating with Thomassen [Tho92[Tho92]Thomassen, Carsten*The Jordan-Schönflies theorem and the classification of surfaces* (1992)The American Mathematical Monthly]). This sketch is more understandable to me but I am less confident in it being a correct proof (e.g., maybe there is some curious fractal curve that causes the diagrammatic proofs to stop being obvious...).
In the special case of the curve $C$ being a polygon, the proof involves "walking along a simple polygonal arc (close to $C$ but not intersecting $C$)" and Hales notes:

Nobody doubts the correctness of this argument. Every mathematician knows how to walk without running in to walls. Detailed figures indicating how to "walk along a simple polygonal arc" would be superfluous, if not downright insulting. Yet, it is quote another matter altogether to train a computer to run around a maze-like polygon without collisions...

These observations demonstrate how one's confidence in a mathematical result is not merely a formal affair but includes ostensibly informal arguments of correctness. This corobborates the attitude taken be De Millo *et al* in Section 2.6.1. Additionally, as noted in Section 1.1, confidence in results also includes a social component: a mathematician will be more confident that a result is correct if that result is well established within the field.

There has also been some empirical work on the question of confidence in proofs. Inglis and Alcock [IA12[IA12]Inglis, Matthew; Alcock, Lara*Expert and novice approaches to reading mathematical proofs* (2012)Journal for Research in Mathematics Education] performed an empirical study on eye movements in undergrads vs postgrads. A set of undergraduates and post-graduate researchers were presented with a set of natural language proofs and then asked to judge the validity of these proofs. The main outcomes they suggest from their work are that mathematicians can disagree about the validity of even short proofs and that post-graduates read proofs in a different way to undergraduates: moving their focus back and forth more. This suggests that we might expect undergraduates and postgraduates to present different reasons for their confidence in the questions.

## 2.6.3. Understandability and confidence within automated theorem proving.

The concepts of understandability and confidence have also been studied empirically within the context of proof assistants. This will be picked up in Chapter 6.

Stenning *et al.* [SCO95[SCO95]Stenning, Keith; Cox, Richard; *et al.**Contrasting the cognitive effects of graphical and sentential logic teaching: reasoning, representation and individual differences* (1995)Language and Cognitive Processes] used the graphical *Hyperproof* software (also discussed in Section 2.5) to compare graphical and sentence-based representations in the teaching of logic.
They found that both representations had similar transferabilityThat is, do lessons learnt in one domain transfer to anologous problems in other domains?
The psychological literature identifies this as a difficult problem in teaching. and that the best teaching representation (in terms of test scores) was largely dependent on the individual differences between the students.
This suggests that in looking for what it means for a proof to be understandable, we should not forget that people have different ways of thinking about proofs, and so there is not going to be a one-size-fits-all solution. It also suggests that providing multiple ways of conceptualising problems should help with understandability.

In Grebing's thesis [Gre19[Gre19]Grebing, Sarah Caecilia*User Interaction in Deductive Interactive Program Verification* (2019)], a set of focus groups are conducted to ask a set of users with a variety of experience-levels in Isabelle and KeY, to reflect on the user interfaces.
One of her main findings was that due to the extensive levels of automation in the proving process, there can arise a 'gap' between the user's model of the proof state and the proof state created through the automation.
Grebing then provides a bridge for this gap in the form of a proof scripting language and user interface for the KeY prover at a higher level of abstraction than the existing interface.
Grebing also provides a review of other empirical studies conducted on the user interfaces of proof assistants [Gre19 §6.2.0].

# 2.7. Human-like reasoning

How should a prover work to produce human-like mathematical reasoning? The easiest answer is: however humans think it should reason!

The very earliest provers such as the Boyer-Moore theorem prover [BM73[BM73]Boyer, Robert S.; Moore, J. Strother*Proving Theorems about LISP Functions* (1973)IJCAI, BM90[BM90]Boyer, Robert S; Moore, J Strother*A theorem prover for a computational logic* (1990)International Conference on Automated Deduction, BKM95[BKM95]Boyer, Robert S; Kaufmann, Matt; *et al.**The Boyer-Moore theorem prover and its interactive enhancement* (1995)Computers & Mathematics with Applications] take this approach to some extent; the design being steered through a process of introspection on how the authors would prove theorems.
Although with their 'waterfall' architecture, the main purpose is to prove theorems automatically, rather than creating proofs that a human could follow.
Indeed Robinson's machine-like resolution method [BG01[BG01]Bachmair, Leo; Ganzinger, Harald*Resolution theorem proving* (2001)Handbook of automated reasoning] was such a dominant approach that Bledsoe titled his paper *non-resolution theorem proving* [Ble81[Ble81]Bledsoe, Woodrow W*Non-resolution theorem proving* (1981)Readings in Artificial Intelligence]. Another early work on human-oriented reasoning is that of Nevins [Nev74[Nev74]Nevins, Arthur J*A human oriented logic for automatic theorem-proving* (1974)Journal of the ACM (JACM)], similar to this theis, Nevins is motivated by the desire to make proofs more understandable to mathematicians.
Some examples of prover automation that are designed to perform moves that a human would do are `grind`

for PVShttp://pvs.csl.sri.com/ [SORS01[SORS01]Shankar, Natarajan; Owre, Sam; *et al.**PVS prover guide* (2001)Computer Science Laboratory, SRI International, Menlo Park, CA] and the waterfall algorithm in ACL2https://www.cs.utexas.edu/users/moore/acl2/ [KMM13[KMM13]Kaufmann, Matt; Manolios, Panagiotis; *et al.**Computer-aided reasoning: ACL2 case studies* (2013)].

My own journey into this field started with reading the work of Gowers and Ganesalingam (G&G) in their Robot prover [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.*A fully automatic theorem prover with human-style output* (2017)J. Automated Reasoning]A working fork of this can be found at https://github.com/edayers/robotone..
G&G's motivation was to find a formal system that better represented the way that a human mathematician would solve a mathematics problem, demonstrating this through the ability to generate realistic natural-language write-ups of these proofs.
The system made use of a natural-deduction style hierarchical proof-state with structural sharing.
The inference rules (called 'moves') on these states and the order in which they were invoked were carefully chosen through an introspective process.

A different approach to exploring human-like reasoning is by modelling the process of mathematical discourse.
Pease, Cornelli, Martin, *et al* [CMM+17[CMM+17]Corneli, Joseph; Martin, Ursula; *et al.**Modelling the way mathematics is actually done* (2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, PLB+17[PLB+17]Pease, Alison; Lawrence, John; *et al.**Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation* (2017)Artificial Intelligence] have investigated the use of graphical discourse models of mathematical reasoning.
In this thesis, however I have restricted the scope to human-like methods for solving simple lemmas that can produce machine-checkable proofs.

Another key way in which humans reason is through the use of diagrams and alternate representations of things. A *prima facie* unintuitive result such as $1+2+3+⋯+n=21 n(n+1)$ snaps together when presented with the appropriate representation Figure 2.29.
Some recent work investigating and automating this process is the rep2rep project [RSS+20[RSS+20]Raggi, Daniel; Stapleton, Gem; *et al.**How to (Re)represent it?* (2020)32nd IEEE International Conference on Tools with Artificial Intelligence].
Jamnik's previous work also explores how one can perform automated reasoning on the domain of diagrams
[Jam01[Jam01]Jamnik, Mateja*Mathematical Reasoning with Diagrams: From Intuition to Automation* (2001)]. This is an important feature of general human-like reasoning, however I will not explore representations further in this thesis.

## 2.7.1. Higher levels of abstraction

There have been many previous works which add higher-level abstraction layers atop an existing prover with the aim of making a prover that is more human-like.

Archer *et al.* developed the *TAME* system for the PVS prover [AH97[AH97]Archer, Myla; Heitmeyer, Constance*Human-style theorem proving using PVS* (1997)International Conference on Theorem Proving in Higher Order Logics].
Although they were focussed on proving facts about software rather than mathematics, a lot of the goals are similar.
*TAME* makes use of a higher abstraction level. However it is only applied to reasoning about timed automatahttps://en.wikipedia.org/wiki/Timed_automaton and doesn't include a user study.

As part of the `auto2`

prover tactic for Isabelle, Zhan [Zha16[Zha16]Zhan, Bohua*AUTO2, a saturation-based heuristic prover for higher-order logic* (2016)International Conference on Interactive Theorem Proving] developed a high-level proof script syntax to guide the automation of `auto2`

.
A script takes the form of asserting several intermediate facts for the prover to prove before proving the main goal.
This script is used to steer the `auto2`

prover towards proving the result. This contrasts with tactic-based proof and structural scripts (e.g. Isar [Wen99[Wen99]Wenzel, Makarius*Isar-a generic interpretative approach to readable formal proof documents* (1999)TPHOLs]) which are instead instructions for chaining together tactics.
With the `auto2`

style script, it is possible to omit a lot of the detail that would be required by tactic-based scripts, since steps and intermediate goals that are easy for the automation to solve can be omitted entirely.

## 2.7.2. Proof planning

Proof planning originated with Bundy [Bun88[Bun88]Bundy, Alan*The use of explicit plans to guide inductive proofs* (1988)International conference on automated deduction, Bun98[Bun98]Bundy, Alan*Proof planning* (1998)] and is the application of performing a proof with respect to a high-level plan (e.g., I am going to perform induction then simplify terms) that is generated before low-level operations commence (performing induction, running simplification algorithms). The approach follows the general field of AI planning.

AI planning in its most general conception [KKY95[KKY95]Kambhampati, Subbarao; Knoblock, Craig A; *et al.**Planning as refinement search: A unified framework for evaluating design tradeoffs in partial-order planning* (1995)Artificial Intelligence] is the process of searching a graph `G`

using plan-space rather than by searching it directly.
In a typical planning system, each point in plan-space is a DAGDirected Acyclic Graph of objects called **ground operators** or **methods**, each of which has a mapping to paths in `G`

.
Each ground operator is equipped with predicates on the vertices of `G`

called **pre/post-conditions**.
Various AI planning methods such as GRAPHPLAN [BF97[BF97]Blum, Avrim L; Furst, Merrick L*Fast planning through planning graph analysis* (1997)Artificial intelligence] can be employed to discover a partial ordering of these methods, which can then be used to construct a path in `G`

.
This procedure applied to the problem of finding proofs is proof planning.
The main issue with proof planning [Bun02[Bun02]Bundy, Alan*A critique of proof planning* (2002)Computational Logic: Logic Programming and Beyond] is that it is difficult to identify sets of conditions and methods that do not cause the plan space to be too large or disconnected. However, in this paper we are not trying to construct plans for entire proofs, but just to model the thought processes of humans when solving simple equalities.
A comparison of the various proof planners is provided by Dennis, Jamnik and Pollet [DJP06[DJP06]Dennis, Louise A; Jamnik, Mateja; *et al.**On the Comparison of Proof Planning Systems:, lambdaCLAM, Ωmega and IsaPlanner* (2006)Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning].

Proof planning in the domain of finding equalities frequently involves a technique called **rippling** [BSV+93[BSV+93]Bundy, Alan; Stevens, Andrew; *et al.**Rippling: A heuristic for guiding inductive proofs* (1993)Artificial Intelligence, BBHI05[BBHI05]Bundy, Alan; Basin, David; *et al.**Rippling: meta-level guidance for mathematical reasoning* (2005)], in which an expression is annotated with additional structure determined by the differences between the two sides of the equation that directs the rewriting process.
In our system we avoid using rippling because of our concern for generality: for finding chains of equalities, subtasks achieve similar results and are less tied to particular domains.

Another technique associated with proof planning is the concept of **proof critics** [Ire92[Ire92]Ireland, Andrew*The use of planning critics in mechanizing inductive proofs* (1992)International Conference on Logic for Programming Artificial Intelligence and Reasoning].
Proof critics are programs which take advantage of the information from a failed proof plan to construct a new, amended proof plan.
An interactive version of proof critics has also been developed [IJR99[IJR99]Ireland, Andrew; Jackson, Michael; *et al.**Interactive proof critics* (1999)Formal Aspects of Computing].

Another general AI system that will be relevant to this thesis is **hierarchical task networks** [MS99[MS99]Melis, Erica; Siekmann, Jörg*Knowledge-based proof planning* (1999)Artificial Intelligence, Tat77[Tat77]Tate, Austin*Generating project networks* (1977)IJCAI] which are used to drive the behaviour of artificial agents such as the ICARUS architecture [LCT08[LCT08]Langley, Pat; Choi, Dongkyu; *et al.**Icarus user’s manual* (2008)].
Starting tasks are broken down into subtasks, which are then used to find fine-grained methods for achieving the original tasks.

# 2.8. Natural language for formal mathematics

In this section I will survey the background and related work on using natural language to generate proofs. The material in this chapter will be used in Section 3.6 and Chapter 6.

## 2.8.1. Natural language generation in a wider context

Data-to-text natural language generation (NLG) is a subfield of natural language processing (NLP) that focusses on the problem of computing intelligible natural language discourses and text from some non-textual object (without a human in the loop!). An example is producing an English description of the local weather forecast from meteorological data. NLG techniques can range from simple 'canned text' and 'mail-merge' applications right up to systems with aspirations of generality such as modern voice recognition in smartphones.

There are a wide variety of architectures available for modern NLG [GK18[GK18]Gatt, Albert; Krahmer, Emiel*Survey of the state of the art in natural language generation: Core tasks, applications and evaluation* (2018)Journal of Artificial Intelligence Research], however they usually carry a modular structure, with a backbone [RD00[RD00]Reiter, Ehud; Dale, Robert*Building natural language generation systems* (2000)] being split in to three pipeline stages as shown in Figure 2.30.

**Macro-planner**or**discourse planner**: dictates how to structure the general flow of the text. That is, serialising the input data. These often take the form of 'expert systems' with a large amount of domain specific knowledge encoded**Micro-planner**: determines how the stream of information from the macro-planner should be converted in to individual sentences, how sentences should be structured and determining how the argument should 'flow'.**Realiser**: produces the final text from the abstracted output of the micro-planner. For example, applying punctuation rules and choosing the correct conjugations.

These choices of stages are mainly motivated through a desire to reuse code and to separate concerns (a realiser does not need to know the subject of the text it is correcting the punctuation form).

An alternative approach to the one outlined above is to use statistical methods for natural language generation. The advent of scalable machine learning (ML) and neural networks (NNs) of the 2010s has gained dominance in many NLG tasks such as translation and scene description. The system developed for this work in Section 3.6 is purely classical, with no machine learning component. In the context of producing simple write-ups of proofs, there will likely be some gains from including ML, but it is not clear that a statistical approach to NLG is going to assist in building understandable descriptions of proofs, because it means that there is no way to confirm whether the description generated by a black-box NLG component is going to be related to the input.

## 2.8.2. Natural language generation for mathematics

The first modern study of the linguistics of natural language mathematics is the work of Ranta [Ran94[Ran94]Ranta, Aarne*Syntactic categories in the language of mathematics* (1994)International Workshop on Types for Proofs and Programs, Ran95[Ran95]Ranta, Aarne*Context-relative syntactic categories and the formalization of mathematical text* (1995)International Workshop on Types for Proofs and Programs] concerning the translation between dependent type theory and natural language and I will use some of his insights in Section 3.6. Ganesalingam's thesis [Gan10[Gan10]Ganesalingam, Mohan*The language of mathematics* (2010)] is an excellent reference for understanding the linguistics of mathematics in general, however it is more concerned with natural language input.

There have been numerous previous attempts at creating natural language output from a theorem prover:
Felty-Miller [FM87[FM87]Felty, Amy; Miller, Dale*Proof explanation and revision* (1987)], Holland-Minkley *et al* within the NuPrl proverhttps://nuprl.org [HBC99[HBC99]Holland-Minkley, Amanda M; Barzilay, Regina; *et al.**Verbalization of High-Level Formal Proofs.* (1999)AAAI/IAAI], and also in Theorema [BCJ+06[BCJ+06]Buchberger, Bruno; Crǎciun, Adrian; *et al.**Theorema: Towards computer-aided mathematical theory exploration* (2006)Journal of Applied Logic].
A particularly advanced NLG for provers was Proverb [HF97[HF97]Huang, Xiaorong; Fiedler, Armin*Proof Verbalization as an Application of NLG* (1997)IJCAI (2)] for the Ωmega theorem prover [BCF+97[BCF+97]Benzmüller, Christoph; Cheikhrouhou, Lassaad; *et al.**Omega: Towards a Mathematical Assistant* (1997)Automated Deduction - CADE-14], this system's architecture uses the pipeline in Figure 2.30 and takes as input a proof term generated by the Ωmega toolchain and outputs a natural language sentence.

The process of synthesising natural language is difficult in the general case.
But as Gowers and Ganesalingam (henceforth G&G) [GG17[GG17]Ganesalingam, Mohan; Gowers, W. T.*A fully automatic theorem prover with human-style output* (2017)J. Automated Reasoning] note, the language found in mathematical proofs is much more restricted than a general English text.
At its most basic, a natural language proof is little more than a string of facts from the assumptions to the conclusion.
There is no need for time-sensitive tenses or other complexities that arise in general text.
Proofs are written this way because mathematical proofs are written to be *checked* by a human and so a uniformity of prose is used that minimises the chance of 'bugs' creeping in.
This, combined with a development calculus designed to encourage human-like proof steps, makes the problem of creating mathematical natural language write-ups much more tenable.
I will refer to these non-machine-learning approaches as 'classical' NLG.

A related problem worth mentioning here is the reverse process of NLG: parsing formal proofs and theorem statements from a natural language text.
The two problems are interlinked in that they are both operating on the same grammar and semantics, but parsing raises a distinct set of problems to NLG, particularly around ambiguity [Gan10 ch. 2].
Within mathematical parsing there are two approaches. The first approach is **controlled natural language** [Kuh14[Kuh14]Kuhn, Tobias*A survey and classification of controlled natural languages* (2014)Computational linguistics] as practiced by ForTheL [Pas07[Pas07]Paskevich, Andrei*The syntax and semantics of the ForTheL language* (2007)] and Naproche/SAD [CFK+09[CFK+09]Cramer, Marcos; Fisseni, Bernhard; *et al.**The naproche project controlled natural language proof checking of mathematical texts* (2009)International Workshop on Controlled Natural Language].
Here, a grammar is specified to parse text that is designed to look as close to a natural langauge version of the text as possible.
The other approach (which I will not make use of in this thesis) is in using machine learning techniques, for example the work on parsing natural mathematical texts is the work of Stathopoulos *et al* [ST16[ST16]Stathopoulos, Yiannos A; Teufel, Simone*Mathematical information retrieval based on type embeddings and query expansion* (2016)COLING 2016, SBRT18[SBRT18]Stathopoulos, Yiannos; Baker, Simon; *et al.**Variable Typing: Assigning Meaning to Variables in Mathematical Text* (2018)NAACL-HLT 2018].

# Bibliography for this chapter

- [ABB+16]Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H.; Ulbrich, Mattias
*Deductive Software Verification - The KeY Book*(2016)**volume**10001**publisher**Springer**doi**10.1007/978-3-319-49812-6**isbn**978-3-319-49811-9view online - [ADL10]Aspinall, David; Denney, Ewen; Lüth, Christoph
*Tactics for hierarchical proof*(2010)Mathematics in Computer Science**volume**3**number**3**pages**309--330**publisher**Springerview online - [AH97]Archer, Myla; Heitmeyer, Constance
*Human-style theorem proving using PVS*(1997)International Conference on Theorem Proving in Higher Order Logics**pages**33--48**organization**Springerview online - [ALW07]Aspinall, David; Lüth, Christoph; Winterstein, Daniel
*A framework for interactive proof*(2007)Towards Mechanized Mathematical Assistants**pages**161--175**publisher**Springerview online - [AMM18]Adámek, Jiří; Milius, Stefan; Moss, Lawrence S
*Fixed points of functors*(2018)J. Log. Algebraic Methods Program.**volume**95**pages**41--81**doi**10.1016/j.jlamp.2017.11.003view online - [Asp00]Aspinall, David
*Proof General: A generic tool for proof development*(2000)International Conference on Tools and Algorithms for the Construction and Analysis of Systems**pages**38--43**organization**Springerview online - [BBHI05]Bundy, Alan; Basin, David; Hutter, Dieter; Ireland, Andrew
*Rippling: meta-level guidance for mathematical reasoning*(2005)**volume**56**publisher**Cambridge University Press - [BCF+97]Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg H.; Sorge, Volker
*Omega: Towards a Mathematical Assistant*(1997)Automated Deduction - CADE-14**volume**1249**pages**252--255**editor**McCune, William**publisher**Springer**doi**10.1007/3-540-63104-6_23view online - [BCJ+06]Buchberger, Bruno; Crǎciun, Adrian; Jebelean, Tudor; Kovács, Laura; Kutsia, Temur; Nakagawa, Koji; Piroi, Florina; Popov, Nikolaj; Robu, Judit; Rosenkranz, Markus; Windsteiger, Wolfgang
*Theorema: Towards computer-aided mathematical theory exploration*(2006)Journal of Applied Logic**volume**4**number**4**pages**470--504**publisher**Elsevier**doi**10.1016/j.jal.2005.10.006view online - [BE92]Barwise, Jon; Etchemendy, John
*Hyperproof: Logical reasoning with diagrams*(1992)Working Notes of the AAAI Spring Symposium on Reasoning with Diagrammatic Representationsview online - [BF97]Blum, Avrim L; Furst, Merrick L
*Fast planning through planning graph analysis*(1997)Artificial intelligence**volume**90**number**1-2**pages**281--300**publisher**Elsevierview online - [BG01]Bachmair, Leo; Ganzinger, Harald
*Resolution theorem proving*(2001)Handbook of automated reasoning**pages**19--99**editors**n.b.**publisher**Elsevier - [BGM+13]Bird, Richard; Gibbons, Jeremy; Mehner, Stefan; Voigtländer, Janis; Schrijvers, Tom
*Understanding idiomatic traversals backwards and forwards*(2013)Proceedings of the 2013 ACM SIGPLAN symposium on Haskell**pages**25--36view online - [BJK+16]Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, Wolfgang
*Theorema 2.0: computer-assisted natural-style mathematics*(2016)Journal of Formalized Reasoning**volume**9**number**1**pages**149--185view online - [BKM95]Boyer, Robert S; Kaufmann, Matt; Moore, J Strother
*The Boyer-Moore theorem prover and its interactive enhancement*(1995)Computers & Mathematics with Applications**volume**29**number**2**pages**27--62**publisher**Elsevier - [BM73]Boyer, Robert S.; Moore, J. Strother
*Proving Theorems about LISP Functions*(1973)IJCAI**pages**486--493**editor**Nilsson, Nils J.**publisher**William Kaufmannview online - [BM90]Boyer, Robert S; Moore, J Strother
*A theorem prover for a computational logic*(1990)International Conference on Automated Deduction**pages**1--15**organization**Springerview online - [BN98]Baader, Franz; Nipkow, Tobias
*Term rewriting and all that*(1998)**publisher**Cambridge University Press**isbn**978-0-521-45520-6 - [BSV+93]Bundy, Alan; Stevens, Andrew; Van Harmelen, Frank; Ireland, Andrew; Smaill, Alan
*Rippling: A heuristic for guiding inductive proofs*(1993)Artificial Intelligence**volume**62**number**2**pages**185--253**publisher**Elsevier - [BT98]Bertot, Yves; Théry, Laurent
*A generic approach to building user interfaces for theorem provers*(1998)Journal of Symbolic Computation**volume**25**number**2**pages**161--194**publisher**Elsevierview online - [Bau20]Bauer, Andrej
*What makes dependent type theory more suitable than set theory for proof assistants?*(2020)view onlineMathOverflow answer - [Ble81]Bledsoe, Woodrow W
*Non-resolution theorem proving*(1981)Readings in Artificial Intelligence**pages**91--108**publisher**Elsevierview online - [Bre16]Breitner, Joachim
*Visual theorem proving with the Incredible Proof Machine*(2016)International Conference on Interactive Theorem Proving**pages**123--139**publisher**Springerview online - [Bun02]Bundy, Alan
*A critique of proof planning*(2002)Computational Logic: Logic Programming and Beyond**pages**160--177**publisher**Springerview online - [Bun88]Bundy, Alan
*The use of explicit plans to guide inductive proofs*(1988)International conference on automated deduction**pages**111--120**organization**Springerview online - [Bun98]Bundy, Alan
*Proof planning*(1998)**publisher**University of Edinburgh, Department of Artificial Intelligence - [CFK+09]Cramer, Marcos; Fisseni, Bernhard; Koepke, Peter; Kühlwein, Daniel; Schröder, Bernhard; Veldman, Jip
*The naproche project controlled natural language proof checking of mathematical texts*(2009)International Workshop on Controlled Natural Language**pages**170--186**organization**Springerview online - [CH88]Coquand, Thierry; Huet, Gérard P.
*The Calculus of Constructions*(1988)Inf. Comput.**volume**76**number**2/3**pages**95--120**doi**10.1016/0890-5401(88)90005-3view online - [CMM+17]Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; Pease, Alison; Puzio, Raymond; Rino Nesin, Gabriela
*Modelling the way mathematics is actually done*(2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design**pages**10--19**organization**ACMview online - [Car19]Carneiro, Mario
*Lean's Type Theory*(2019)view online - [DJP06]Dennis, Louise A; Jamnik, Mateja; Pollet, Martin
*On the Comparison of Proof Planning Systems:, lambdaCLAM, Ωmega and IsaPlanner*(2006)Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning**volume**151**number**1**pages**93--110**editors**n.b.**publisher**Elsevier**doi**10.1016/j.entcs.2005.11.025view online - [EUR+17]Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; Avigad, Jeremy; de Moura, Leonardo
*A metaprogramming framework for formal verification*(2017)Proceedings of the ACM on Programming Languages**volume**1**number**ICFP**pages**1--29**publisher**ACM New York, NY, USAview online - [FGM+07]Foster, J Nathan; Greenwald, Michael B; Moore, Jonathan T; Pierce, Benjamin C; Schmitt, Alan
*Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem*(2007)ACM Transactions on Programming Languages and Systems (TOPLAS)**volume**29**number**3**pages**17--es**publisher**ACM New York, NY, USAview online - [FM87]Felty, Amy; Miller, Dale
*Proof explanation and revision*(1987)**number**MS-CIS-88-17**institution**University of Pennsylvaniaview online - [GG17]Ganesalingam, Mohan; Gowers, W. T.
*A fully automatic theorem prover with human-style output*(2017)J. Automated Reasoning**volume**58**number**2**pages**253--291**doi**10.1007/s10817-016-9377-1view online - [GK18]Gatt, Albert; Krahmer, Emiel
*Survey of the state of the art in natural language generation: Core tasks, applications and evaluation*(2018)Journal of Artificial Intelligence Research**volume**61**pages**65--170view online - [GPJ17]Gallego Arias, Emilio Jesús; Pin, Benoît; Jouvelot, Pierre
*jsCoq: Towards Hybrid Theorem Proving Interfaces*(2017)Proceedings of the 12th Workshop on User Interfaces for Theorem Provers**volume**239**pages**15-27**editors**n.b.**publisher**Open Publishing Association**doi**10.4204/EPTCS.239.2view online - [Gal16]Gallego Arias, Emilio Jesús
*SerAPI: Machine-Friendly, Data-Centric Serialization for Coq*(2016)**institution**MINES ParisTechview online - [Gan10]Ganesalingam, Mohan
*The language of mathematics*(2010)**publisher**Springerview online - [Gor00]Gordon, Mike
*From LCF to HOL: a short history*(2000)Proof, language, and interaction**pages**169--186view online - [Gre19]Grebing, Sarah Caecilia
*User Interaction in Deductive Interactive Program Verification*(2019)view online - [HBC99]Holland-Minkley, Amanda M; Barzilay, Regina; Constable, Robert L
*Verbalization of High-Level Formal Proofs.*(1999)AAAI/IAAI**pages**277--284**editors**n.b.**publisher**AAAI Press / The MIT Pressview online - [HF97]Huang, Xiaorong; Fiedler, Armin
*Proof Verbalization as an Application of NLG*(1997)IJCAI (2)**pages**965--972view online - [Hal07]Hales, Thomas C
*The Jordan curve theorem, formally and informally*(2007)The American Mathematical Monthly**volume**114**number**10**pages**882--894**publisher**Taylor & Francisview online - [Hur95]Hurkens, Antonius JC
*A simplification of Girard's paradox*(1995)International Conference on Typed Lambda Calculi and Applications**pages**266--278**organization**Springer - [IA12]Inglis, Matthew; Alcock, Lara
*Expert and novice approaches to reading mathematical proofs*(2012)Journal for Research in Mathematics Education**volume**43**number**4**pages**358--390**publisher**National Council of Teachers of Mathematicsview online - [IJR99]Ireland, Andrew; Jackson, Michael; Reid, Gordon
*Interactive proof critics*(1999)Formal Aspects of Computing**volume**11**number**3**pages**302--325**publisher**Springerview online - [Ire92]Ireland, Andrew
*The use of planning critics in mechanizing inductive proofs*(1992)International Conference on Logic for Programming Artificial Intelligence and Reasoning**pages**178--189**organization**Springerview online - [JR12]Jaskelioff, Mauro; Rypacek, Ondrej
*An Investigation of the Laws of Traversals*(2012)Proceedings Fourth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2012, Tallinn, Estonia**volume**76**pages**40--49**editors**n.b.**doi**10.4204/EPTCS.76.5view online - [Jam01]Jamnik, Mateja
*Mathematical Reasoning with Diagrams: From Intuition to Automation*(2001)**publisher**CSLI Press - [KKY95]Kambhampati, Subbarao; Knoblock, Craig A; Yang, Qiang
*Planning as refinement search: A unified framework for evaluating design tradeoffs in partial-order planning*(1995)Artificial Intelligence**volume**76**number**1**pages**167--238view online - [KMM13]Kaufmann, Matt; Manolios, Panagiotis; Moore, J Strother
*Computer-aided reasoning: ACL2 case studies*(2013)**volume**4**publisher**Springer Science & Business Media - [Kuh14]Kuhn, Tobias
*A survey and classification of controlled natural languages*(2014)Computational linguistics**volume**40**number**1**pages**121--170**publisher**MIT Pressview online - [LCT08]Langley, Pat; Choi, Dongkyu; Trivedi, Nishant
*Icarus user’s manual*(2008)**institution**Institute for the Study of Learning and Expertiseview online - [LD97]Lowe, Helen; Duncan, David
*XBarnacle: Making theorem provers more accessible*(1997)Automated Deduction—CADE-14**pages**404--407**publisher**Springerview online - [LP03]Lämmel, Ralf; Peyton Jones, Simon
*Scrap Your Boilerplate*(2003)Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedings**volume**2895**pages**357**editor**Ohori, Atsushi**publisher**Springer**doi**10.1007/978-3-540-40018-9_23view online - [LR13]Lüth, Christoph; Ring, Martin
*A web interface for Isabelle: The next generation*(2013)International Conference on Intelligent Computer Mathematics**pages**326--329**organization**Springerview online - [MAKR15]de Moura, Leonardo; Avigad, Jeremy; Kong, Soonho; Roux, Cody
*Elaboration in Dependent Type Theory*(2015)CoRR**volume**abs/1505.04324view online - [MKA+15]de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; Van Doorn, Floris; von Raumer, Jakob
*The Lean theorem prover (system description)*(2015)International Conference on Automated Deduction**pages**378--388**organization**Springerview online - [MP08]McBride, Conor; Paterson, Ross
*Applicative programming with effects*(2008)J. Funct. Program.**volume**18**number**1**pages**1--13**doi**10.1017/S0956796807006326view online - [MS99]Melis, Erica; Siekmann, Jörg
*Knowledge-based proof planning*(1999)Artificial Intelligence**volume**115**number**1**pages**65--105**publisher**Elsevierview online - [MUP80]de Millo, Richard A; Upton, Richard J; Perlis, Alan J
*Social processes and proofs of theorems and programs*(1980)The mathematical intelligencer**volume**3**number**1**pages**31--40**publisher**Springerview online - [Mar84]Martin-Löf, Per
*Intuitionistic type theory*(1984)**volume**1**publisher**Bibliopolis**isbn**978-88-7088-228-5view online - [Mic78]Michener, Edwina Rissland
*Understanding understanding mathematics*(1978)Cognitive science**volume**2**number**4**pages**361--383**publisher**Wiley Online Library**doi**https://doi.org/10.1207/s15516709cog0204_3view online - [Mil72]Milner, Robin
*Logic for computable functions description of a machine implementation*(1972)**institution**Stanford Universityview online - [Nev74]Nevins, Arthur J
*A human oriented logic for automatic theorem-proving*(1974)Journal of the ACM (JACM)**volume**21**number**4**pages**606--621**publisher**ACM New York, NY, USAview online - [PLB+17]Pease, Alison; Lawrence, John; Budzynska, Katarzyna; Corneli, Joseph; Reed, Chris
*Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation*(2017)Artificial Intelligence**volume**246**pages**181--219**publisher**Elsevierview online - [PP89]Pfenning, Frank; Paulin-Mohring, Christine
*Inductively defined types in the Calculus of Constructions*(1989)International Conference on Mathematical Foundations of Programming Semantics**pages**209--228**organization**Springerview online - [Pas07]Paskevich, Andrei
*The syntax and semantics of the ForTheL language*(2007)view online - [Pau89]Paulson, Lawrence C
*The foundation of a generic theorem prover*(1989)Journal of Automated Reasoning**volume**5**number**3**pages**363--397**publisher**Springerview online - [Pit20]Pit-Claudel, Clément
*Untangling mechanized proofs*(2020)SLE 2020: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering**pages**155--174**doi**https://doi.org/10.1145/3426425.3426940view online - [Poi14]Poincaré, Henri
*Science and method*(1914)**translator**Halsted, George Bruce**publisher**Amazon (out of copyright)**isbn**978-1534945906view onlineThe version at URL is translated by Francis Maitland - [Pro13]The Univalent Foundations Program
*Homotopy Type Theory: Univalent Foundations of Mathematics*(2013)**publisher**Institute for Advanced Studyview online - [Pól62]Pólya, George
*Mathematical Discovery*(1962)**publisher**John Wiley & Sonsview online - [RD00]Reiter, Ehud; Dale, Robert
*Building natural language generation systems*(2000)**publisher**Cambridge university pressview online - [RSS+20]Raggi, Daniel; Stapleton, Gem; Stockdill, Aaron; Jamnik, Mateja; Garcia, Grecia Garcia; Cheng, Peter C.-H.
*How to (Re)represent it?*(2020)32nd IEEE International Conference on Tools with Artificial Intelligence**pages**1224--1232**publisher**IEEE**doi**10.1109/ICTAI50040.2020.00185view online - [Ran94]Ranta, Aarne
*Syntactic categories in the language of mathematics*(1994)International Workshop on Types for Proofs and Programs**pages**162--182**organization**Springerview online - [Ran95]Ranta, Aarne
*Context-relative syntactic categories and the formalization of mathematical text*(1995)International Workshop on Types for Proofs and Programs**pages**231--248**organization**Springerview online - [Ros53]Rosser, J. Barkley
*Logic for Mathematicians*(1953)**publisher**McGraw-Hill**isbn**978-0-486-46898-3 - [SBRT18]Stathopoulos, Yiannos; Baker, Simon; Rei, Marek; Teufel, Simone
*Variable Typing: Assigning Meaning to Variables in Mathematical Text*(2018)NAACL-HLT 2018**pages**303--312**editors**n.b.**publisher**Association for Computational Linguistics**doi**10.18653/v1/n18-1028view online - [SCO95]Stenning, Keith; Cox, Richard; Oberlander, Jon
*Contrasting the cognitive effects of graphical and sentential logic teaching: reasoning, representation and individual differences*(1995)Language and Cognitive Processes**volume**10**number**3-4**pages**333--354**publisher**Taylor & Francisview online - [SHB+99]Siekmann, Jörg; Hess, Stephan; Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fiedler, Armin; Horacek, Helmut; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Pollet, Martin; Sorge, Volker
*LOUI: Lovely OMEGA user interface*(1999)Formal Aspects of Computing**volume**11**number**3**pages**326--342**publisher**Springerview online - [SORS01]Shankar, Natarajan; Owre, Sam; Rushby, John M; Stringer-Calvert, Dave WJ
*PVS prover guide*(2001)Computer Science Laboratory, SRI International, Menlo Park, CAview online - [SP82]Smyth, Michael B; Plotkin, Gordon D
*The category-theoretic solution of recursive domain equations*(1982)SIAM Journal on Computing**volume**11**number**4**pages**761--783**publisher**SIAMview online - [ST16]Stathopoulos, Yiannos A; Teufel, Simone
*Mathematical information retrieval based on type embeddings and query expansion*(2016)COLING 2016**pages**2344--2355**editors**n.b.**publisher**ACLview online - [Sie90]Sierpinska, Anna
*Some remarks on understanding in mathematics*(1990)For the learning of mathematics**volume**10**number**3**pages**24--41**publisher**FLM Publishing Associationview online - [Sie94]Sierpinska, Anna
*Understanding in mathematics*(1994)**volume**2**publisher**Psychology Press - [Spi11]Spiwack, Arnaud
*Verified computing in homological algebra, a journey exploring the power and limits of dependent type theory*(2011)view online - [Spi87]Spinoza, Benedict
*The chief works of Benedict de Spinoza*(1887)**translator**Elwes, R.H.M.view online - [Ste17]Steele Jr., Guy L.
*It's Time for a New Old Language*(2017)view onlineInvited talk at Clojure/Conj 2017. Slides: http://groups.csail.mit.edu/mac/users/gjs/6.945/readings/Steele-MIT-April-2017.pdf - [Tat77]Tate, Austin
*Generating project networks*(1977)IJCAI**pages**888--893**organization**Morgan Kaufmann Publishers Inc.view online - [Tho92]Thomassen, Carsten
*The Jordan-Schönflies theorem and the classification of surfaces*(1992)The American Mathematical Monthly**volume**99**number**2**pages**116--130**publisher**Taylor & Francisview online - [VKB18]Vicary, Jamie; Kissinger, Aleks; Bar, Krzysztof
*Globular: an online proof assistant for higher-dimensional rewriting*(2018)Logical Methods in Computer Science**volume**14**publisher**Episciences.orgview onlineproject website: http://ncatlab.org/nlab/show/Globular - [Wen12]Wenzel, Makarius
*Isabelle/jEdit-A Prover IDE within the PIDE Framework.*(2012)AISC/MKM/Calculemus**pages**468--471**organization**Springerview online - [Wen99]Wenzel, Makarius
*Isar-a generic interpretative approach to readable formal proof documents*(1999)TPHOLs**volume**99**pages**167--184**organization**Springer - [Zha16]Zhan, Bohua
*AUTO2, a saturation-based heuristic prover for higher-order logic*(2016)International Conference on Interactive Theorem Proving**pages**441--456**organization**Springerview online - [deB72]de Bruijn, Nicolaas Govert
**volume**75**number**5**pages**381--392**organization**North-Hollandview online