For the experimental user study, the participants were given a training document and a form to fill in. In this appendix I reproduce the form that they saw with some formatting changes.

# D.1. Advertising email

Sent on the 5th October 2020 to the University of Cambridge mathematics mailing list.

Help us learn how mathematicians think and get a £10 amazon voucher!

We are looking for undergraduate and postgraduate mathematics students to participate in a study to help us understand how mathematicians think about proofs.

In the study, we will be asking you to read and rate various proofs of some lemmas from Part IA Group Theory and IB Metric and Topological Spaces, including some proofs which have been formally checked by a computer. You won't need to prove any of the lemmas yourself. The experiment will be on Zoom and take about an hour. As sweetening, you will recieve a £10 Amazon voucher for participating!

To find out more, or to be part of our study, email Edward Ayers at e.w.ayers@maths.cam.ac.uk

# D.2. Training Document

Lean is a computer program that can be used to create and verify mathematical proofs.

This document is a reference to help understand the proofs given in the experiment.

## D.2.1. Expressions

Some of the proofs will use a logical system called *dependent type theory.* In contrast to set theory, this means that every term `x`

has a type `T`

written as `x : T`

. For example

Definitions are created with the `def`

command:

## D.2.2. Propositions

Propositions have the type `Prop`

, and given `P : Prop`

and `Q : Prop`

, we can write:

`P ∧ Q`

for`P`

and`Q`

`P ∨ Q`

for`P`

or`Q`

`P → Q`

for`P`

implies`Q`

. Note arrows associate on the right, so`P → Q → R`

is`P → (Q → R)`

.`∀ (x : X) (ε : ℝ), P`

for all`x : X`

and`ε : ℝ`

we have`P`

.`∃ (x : X), P`

: there exists an`x`

such that`P`

Propositions are themselves types, so if we have `h : P`

, we can read this as saying `h`

is a proof of `P`

. Instead of using a name like `h`

, we can also reference propositions using `‹ ›`

: for example `‹4 < 5›`

to refer to the proof that `4`

is less than `5`

.

## D.2.3. Sets

Given a type `X`

, we can make the type `set X`

of sets of elements of `X`

. Given `A : set X`

, and `a : X`

we can write `a ∈ A`

to be the proposition that `a`

belongs to set `A`

. The usual set theoretical operations still apply;

the empty set

`∅ : set X`

union

`A ∪ B`

intersection

`A ∩ B`

set comprehension

`{a : ℕ | a > 4}`

to mean the set of naturals`a : ℕ`

such that`a > 4`

.

## D.2.4. Tactic notation

Tactic notation is used to prove theorems, there are many tactics which will be explained as they come up.

The lines between `begin`

and `end`

are called *commands* and are used to change the *goal state* of the proof.

## D.2.5. Reference table for tactics

Name | Description | Example | Before | After |
---|---|---|---|---|

`assume` | Unwraps a forall or implication goal. | `assume h : P` | `⊢ P → Q` | `(h : P) ⊢ Q` |

`assume ε : ℝ` | `⊢ ∀ (ε : ℝ), ε + 1 > ε` | `(ε : ℝ) ⊢ ε + 1 > ε` | ||

`show` | State the current goal. Doesn't change the goal state. | `show P` | `⊢ P` | `⊢ P` |

`have` | Make a new goal for`P` | `have h : P` | `⊢ Q` | `⊢ P, (h:P) ⊢ Q` |

`obtain` | Similar to have. Make a new goal for`P` and eliminate `∃` and `∧` | `obtain ⟨x, h₁, h₂⟩ : ∃ (x : X), P ∧ Q` | `⊢ R` | `⊢ ∃ (x : X), P ∧ Q, (x : X) (h₁ : P) (h₂ : Q) ⊢ R` |

`use` | Gives a value for an`∃` goal. | `use 5` | `⊢ ∃ (ε : ℝ), ε > 0` | `⊢ 5 > 0` |

`apply` | Apply the given expression to the goal. | `apply ‹P → Q›` | `⊢ Q` | `⊢ P` |

`split` | Splits an`∧` goal. | `split` | `⊢ P ∧ Q` | `⊢ P, ⊢ Q` |

`calc` | Used to write out a chain of equalities and inequalities. |
| `(h : 5 = x) ⊢ 4 < x` | `done` |

`let` | Defines a new constant. | `let x := 5` | `⊢ P` | `⊢ P` |

`rewrite` | Rewrites an expression with the given equation. | `rewrite ‹x = y›` | `⊢ x + y < 4` | `⊢ x + x < 4` |

`cases` | Splits an 'or' hypothesis in to a pair of cases. | `cases h` | `(h : P ∨ Q) ⊢ R` | `P ⊢ R, Q ⊢ R` |

Splits an 'and' hypothesis in to a pair of hypotheses | `cases h` | `(h : P ∧ Q) ⊢ R` | `(h_l : P), (h_r : Q) ⊢ R` | |

`finish` | Tries to solve the goal by repeatedly applying assumptions. | `finish` | ||

`simp` | Tries to solve the goal by simplifying expressions | `simp` | ||

`norm_num` | Solves various simple number problems. | `norm_num` | `⊢ 5 > 0` | `done` |

`ring` | Tries to normalise and solve equations and inequalities in rings. | `ring` | `⊢ (x + y)² = x² + 2 * x * y + y²` | `done` |

`assumption` | Find a previous assume or have result that achieves the goal | `assumption` | `(h :P) ⊢ P` | `done` |

# D.3. Proof scripts

**note:** any paragraphs prepended with "**note:**" are not seen by the experiment participants. Additionally, the order in which they were presented the proofs and lemmas was randomised for each participant, with the exception of Lemma 1 which was always shown first.

## D.3.1. Lemma 1. The composition of group homomorphisms is a group homomorphism.

The composition of two group homomorphisms is a group homomorphism.

### D.3.1.1. Definitions

Here we write the group product on two group elements `x y : G`

as `x * y`

and write `x⁻¹ :G`

as the inverse element of `x`

. The identity is written as `e : G`

.

Given a pair of groups `G`

, `H`

, a function `f : G → H`

is a **group homomorphism** whenever `f (x * y) = f x * f y`

for all `x y ∈ G`

.

### D.3.1.2. Proof A

### D.3.1.3. Proof B

Let `G`

, `H`

and `I`

be groups and let `f : G → H`

and `g : H → I`

where `f`

and `g`

are group homomorphisms. Let `x`

and `y`

be elements of `G`

. Since `f`

and `g`

are group homomorphisms, we have

We are done.

### D.3.1.4. Proof C

**note:** Adapted from Dexter Chua's notes on IA Group Theoryhttps://dec41.user.srcf.net/notes/ [Chu18[Chu18]Chua, Dexter*Cambridge Notes* (2018)].

Let `f : G → H`

and `g : H → I`

be group homomorphisms and let `x`

and `y`

be elements of `G`

. Then we have

and we are done.

## D.3.2. Lemma 2. The union of two open sets is open.

### D.3.2.1. Definitions

Recall that a metric space is a type `X`

equipped with a distance function

such that the following properties hold:

`dist x x = 0`

for all`x : X`

`dist x y = dist y x`

for all`x y : X`

`dist x z ≤ dist x y + dist y z`

for all`x y z : X`

We say a subset `A : set X`

is **open** when

### D.3.2.2. Proof A

### D.3.2.3. Proof B

Let `X`

be a metric space and `A`

, `B`

be sets on `X`

. Assume `A`

and `B`

are open. Let `y ∈ A ∪ B`

. We must choose `ε > 0`

such that `∀ (x : X), dist x y < ε → x ∈ A ∪ B`

. Let `x`

be a point in `X`

where `dist x y < ε`

. We must show that `x ∈ A ∪ B`

. Since `y ∈ A ∪ B`

, either `y ∈ A`

or `y ∈ B`

.

In the case `y ∈ A`

: Since `A ⊆ A ∪ B`

, it suffices to show `x ∈ A`

. Since `A`

is open and `y ∈ A`

, there exists `η > 0`

such that `x ∈ A`

whenever `dist x y < η`

. Therefore, setting `ε`

to be `η`

we are done.

In the case `y ∈ B`

: Since `B ⊆ A ∪ B`

, it suffices to show `x ∈ B`

. Since `B`

is open and `y ∈ B`

, there exists `θ > 0`

such that `x ∈ B`

whenever `dist x y < θ`

. Therefore, setting `ε`

to be `θ`

we are done.

### D.3.2.4. Proof C

**note:** Adapted from *Measure, Topology and Fractal Geometry* by Gerald Edgar [Edg07[Edg07]Edgar, Gerald*Measure, topology, and fractal geometry* (2007)].

Let `y ∈ A ∪ B`

. Then either `y ∈ A`

or `y ∈ B`

. In the case that `y ∈ A`

, there is some `ε > 0`

such that for all `x : X`

, `dist x y < ε`

implies `x ∈ A`

. Similarly for `y ∈ B`

. So `A ∪ B`

is an open set.

## D.3.3. Lemma 3. The kernel of a group homomorphism is a normal subgroup.

### D.3.3.1. Definitions

Given groups `G`

and `H`

and a function `f : G → H`

, `f`

is a group homomorphism if we have `f (x * y) = (f x) * (f y)`

for all `x`

, `y`

in `G`

. If `f`

is a group homomorphism then it may also be shown that `f e = e`

(where `e`

is the identity element) and `f (x⁻¹) = (f x)⁻¹`

.

Define the **kernel** of `f`

to be the set `{k : G | f k = e}`

. It can be shown that the kernel of `f`

is a subgroup of `G`

.

A subgroup `K`

of `G`

is said to be **normal** when for all `k ∈ K`

and all `g : G`

, we have `g * k * g⁻¹ ∈ K`

.

### D.3.3.2. Proof A

### D.3.3.3. Proof B

Let `k ∈ kernel f`

and `g`

be an element of `G`

. We must show `f (g * k * g⁻¹) = e`

. Since `f k = e`

, we have

We are done.

### D.3.3.4. Proof C

**note:** Adapted from Dexter Chua's notes on IA Group Theoryhttps://dec41.user.srcf.net/notes/

Given homomorphism `f : H → G`

, and some `g : G`

, for all `k ∈ kernel f`

, we have `f (g * k * g⁻¹) = f g * f k * (f g)⁻¹ = f g * e * (f g)⁻¹ = e`

. Therefore `g * k * g⁻¹ ∈ kernel f`

by definition of the kernel.

## D.3.4. Lemma 4. The intersection of two open sets is open.

### D.3.4.1. Proof A

### D.3.4.2. Proof B

Let `y`

be an element of `A ∩ B`

. Then `y ∈ A`

and `y ∈ B`

. Therefore, since `A`

is open, there exists `η > 0`

such that `x ∈ A`

whenever `dist x y < η`

and since `B`

is open, there exists `θ > 0`

such that `x ∈ B`

whenever `dist x y < θ`

. We must choose `ε > 0`

such that `x ∈ A ∩ B`

whenever `dist x y < ε`

. Suppose `dist x y < ε`

. Then `dist x y < η`

if `ε ≤ η`

and `dist x y < θ`

if `ε ≤ θ`

. We are done by setting `ε`

to be `min η θ`

.

### D.3.4.3. Proof C

**note:** Adapted from *Measure, Topology and Fractal Geometry* by Gerald Edgar [Edg07[Edg07]Edgar, Gerald*Measure, topology, and fractal geometry* (2007)].

Suppose `A`

and `B`

are both open. Let `y ∈ A ∩ B`

. Since `A`

is open, there is `η > 0`

with `dist x y < η → x ∈ A`

for all `x`

. Also, since `B`

is open, there is `θ > 0`

with `dist x y < θ → x ∈ B`

for all `x`

. Therefore, if `ε`

is the minimum of `η`

and `θ`

, then we have `x ∈ A ∩ B`

whenever `dist x y < ε`

for all `x`

. So `A ∩ B`

is an open set.

# D.4. Consent form

Each participant signed this form before their session started.

This study is part of my PhD research on creating better proof assistant tools for mathematicians.

I am interested in how people compare proofs of theorems created using a proof assistant and created using natural language.

The experiment consists of 4 rounds. In each round you will be asked to compare and evaluate a set of proofs for the same mathematical lemma. Some of the proofs are written in Lean, software for creating formally verified proofs and others are written in the style of natural language. Before the experiment starts there will be a brief training phase on the syntax of Lean. After the experiment, there will be a debrief phase involving some discussion and a brief questionnaire.

Please note that none of the tasks are a test of you or your mathematical ability; the goal is to understand the properties of proofs that you find understandable and useful.

The experiment will be conducted remotely via Zoom. Please use a desktop OS such as Linux, macOS or Windows with a copy of Zoom installed. Please make sure that you are in a quiet environment suitable for a meeting.

## D.4.1. Confidentiality

The following data will be recorded:

name

email address

audio or video recording of the experiment

These will only be used to communicate with you, or better understand your responses and will only be visible to me, the experimenter. If video is recorded, it will be deleted immediately after the experiment and only the audio will be kept. Your name, email and recordings will never be publicly released and will be deleted by 1st February 2021.

Additionally, the following data during the experiment will be textually recorded and anonymised.

Your answers to the forms and surveys during the experiment.

Any verbal answers and comments you give during the experiment. Note that you can explicitly request for me to discard any of these if you wish.

Transcripts of quotes from the audio recording may be publicly released.

These may be released publicly but your anonymity will be protected in any papers, peer review, institutional repositories and presentations that result from this work.

## D.4.2. Finding out about the results

If interested, you can email me at edward.ayers@outlook.com in 2021 to hear about the results of the study.

## D.4.3. Record of consent

Your signature below indicates that you have understood the information about the experiment and consent to your participation. The participation is voluntary and you may refuse to answer certain questions and withdraw from the study and request your data be deleted at any time with no penalty. This does not waive your legal rights. You should have received a copy of the consent form for your own record. If you have further questions related to this research, please contact me at edward.ayers@outlook.com.

# Bibliography for this chapter

- [Chu18]Chua, Dexter
*Cambridge Notes*(2018)view onlineGitHub: https://github.com/dalcde/cam-notes - [Edg07]Edgar, Gerald
*Measure, topology, and fractal geometry*(2007)**publisher**Springer Science and Business Media