Appendix D
Material for evaluation study

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.

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.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.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 Theory [Chu18[Chu18]Chua, DexterCambridge Notes (2018)https://dec41.user.srcf.net/notes].

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.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, GeraldMeasure, topology, and fractal geometry (2007)publisher Springer].

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.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 Theory

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.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, GeraldMeasure, topology, and fractal geometry (2007)publisher Springer].

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

• 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.

• 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.