E.W.Ayers
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.

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

(D.1).
-- this is a comment
4 :-- 4 is natural number
ε :-- ε is a real number
f : X → Y -- f has the type of a function from X to Y

Definitions are created with the def command:

(D.2).
def my_function (x y : ) := x * x + y
my_function 4 5 -- returns 21

D.2.2. Propositions

Propositions have the type Prop, and given P : Prop and Q : Prop , we can write:

  • PQ for P and Q

  • PQ for P or Q

  • PQ for P implies Q. Note arrows associate on the right, so PQR is P(QR).

  • (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 aA to be the proposition that a belongs to set A. The usual set theoretical operations still apply;

  • the empty set : set X

  • union AB

  • intersection AB

  • 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).
theorem an_example : ((x :), x > 3)((y :), y > 4) :=
begin
-- introduce an assumption
assume h: (x, x > 3),
-- obtain x from the assumption
obtainx, h₂⟩ :x, x > 3,
{ from h,
},
-- remind ourselves of the goal
show(y :), y > 4,
-- choose y to be x + 1
use x + 1,
-- show that x + 1 > 4 using a calculation
calc x + 1 > 3 + 1 : by apply nat.add_lt_add_right h1
... = 4 : by norm_num
end

D.2.5. Reference table for tactics

TODO; fix formatting!

NameDescriptionExampleBeforeAfter
assumeUnwraps a forall or implication goal.assume h : PPQ(h : P)Q
assume ε : ⊢ ∀ (ε : ), ε + 1 > ε (ε : )ε + 1 > ε
showState the current goal. Doesn't change the goal state.show PPP
haveMake a new goal forPhave h : PQP, (h:P)Q
obtainSimilar to have. Make a new goal forP and eliminate and obtainx, h₁, h₂:(x : X), PQ R⊢ ∃ (x : X), PQ, (x : X) (h₁ : P) (h₂ : Q)R
useGives a value for an goal.use 5⊢ ∃ (ε : ), ε > 05 > 0
applyApply the given expression to the goal.applyPQQP
splitSplits an goal.splitPQP,Q
calcUsed to write out a chain of equalities and inequalities.
calc 4 < 5 : by norm_num
(h : 5 = x)4 < x done
letDefines a new constant.let x := 5P P
rewriteRewrites an expression with the given equation.rewritex = yx + y < 4x + x < 4
casesSplits an 'or' hypothesis in to a pair of cases.cases h(h : PQ)RPR, QR
Splits an 'and' hypothesis in to a pair of hypothesescases h(h : PQ)R(h_l : P), (h_r : Q)R
finishTries to solve the goal by repeatedly applying assumptions.finish
simpTries to solve the goal by simplifying expressionssimp
norm_numSolves various simple number problems.norm_num5 > 0done
ringTries to normalise and solve equations and inequalities in rings.ring(x + y)² = x² + 2 * x * y + y²done
assumptionFind a previous assume or have result that achieves the goalassumption(h :P)Pdone

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 : GH is a group homomorphism whenever f (x * y) = f x * f y for all x yG.

(D.4).
variables {G H I : Type} [group G] [group H] [group I]
variables {f : G → H} {g : H → I}
def is_hom (f : G → H) :=(x y : G), f (x * y) = f x * f y
(gf) x := g (f (x))

D.3.1.2. Proof A

(D.5).
theorem hom_composition : is_hom fis_hom gis_hom (gf) :=
begin
assume hf : is_hom f,
assume hg : is_hom g,
assume x y : G,
calc g (f (x * y)) = g (f x * f y) : by rewrite hf
... = (g (f x)) * (g (f y)) : by rewrite hg,
end

D.3.1.3. Proof B

Let G, H and I be groups and let f : GH and g : HI where f and g are group homomorphisms. Let x and y be elements of G. Since f and g are group homomorphisms, we have

(D.6).
(gf)(x * y) = g(f(x * y))
= g(f(x) * f(y))
= g(f(x)) * g(f(y))
= (gf)(x) * g(f(y))
= (gf)(x) * (gf)(y)

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, DexterCambridge Notes (2018)].

Let f : GH and g : HI be group homomorphisms and let x and y be elements of G. Then we have

(D.7).
(gf)(x * y) = g(f(x * y))
= g(f(x) * f(y))
= g(f(x)) * g(f(y))
= (gf)(x) * (gf)(y)

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

(D.8).
dist : X → X → ℝ

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 zdist x y + dist y z for all x y z : X

We say a subset A : set X is open when

(D.9).
(x : X), (x ∈ A) → ∃ (ε :), (ε > 0) ∧ ∀ (y : X), dist y x < ε → y ∈ A

D.3.2.2. Proof A

(D.10).
example : is_open A → is_open B → is_open (A ∪ B) :=
begin
assume h: is_open A
assume h: is_open B,
assume y : X,
assume h: y ∈ A ∪ B,
casesy ∈ A ∪ B›,
{ -- in the case that y ∈ A
obtain ⟨η, η_pos, h₄⟩ : ∃ η, (η > 0) ∧ ∀ x, dist x y < η → x ∈ A,
{ applyis_open A›,
applyy ∈ A›,
},
show ∃ ε, (ε > 0) ∧ ∀ x, dist x y < ε → x ∈ A ∪ B,
use [η, η_pos],
showx, dist x y < η → x ∈ A ∪ B,
assume x : X,
assume h: dist x y < η,
show x ∈ A ∪ B,
apply set.subset_union_left, -- A ⊆ A ∪ B
show x ∈ A,
finish,
}, { -- in the case that y ∈ B
obtain ⟨θ, θ_pos, h_θ⟩ : ∃ θ, (θ > 0) ∧ ∀ x, dist x y < θ → x ∈ B,
{ applyis_open B›,
applyy ∈ B›,
},
use [θ, θ_pos],
assume x : X,
assume h: dist x y < θ,
apply set.subset_union_right, -- B ⊆ A ∪ B
finish,
}
end

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 yAB. We must choose ε > 0 such that (x : X), dist x y < εxAB. Let x be a point in X where dist x y < ε. We must show that xAB. Since yAB, either yA or yB.

In the case yA: Since AAB, it suffices to show xA. Since A is open and yA, there exists η > 0 such that xA whenever dist x y < η. Therefore, setting ε to be η we are done.

In the case yB: Since BAB, it suffices to show xB. Since B is open and yB, there exists θ > 0 such that xB 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)].

Let yAB. Then either yA or yB. In the case that yA, there is some ε > 0 such that for all x : X, dist x y < ε implies xA. Similarly for yB. So AB 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 : GH , 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 kK and all g : G, we have g * k * g⁻¹ ∈ K.

(D.11).
variables {G : Type} [group G]
variables {H : Type} [group H]
def is_hom (f : G → H) :=
(x y : G), f (x * y) = f x * f y
variables {f : G → H} [is_hom f]
def is_hom.one : f e = e := -- proof ommitted
def is_hom.inv :(x : G), f (x⁻¹) = (f x)⁻¹ := -- proof ommitted
def kernel (f : G → H) [is_hom f] : subgroup G :=
{k : G | f k = e},
... -- proof that the kernel is a subgroup ommitted
def is_normal (K : subgroup G) :=
(k : G), (k ∈ K) → ∀ (g : G), g * k * g⁻¹ ∈ K

D.3.3.2. Proof A

(D.12).
theorem kernel_is_normal : is_normal (kernel f) :=
begin
assume k : G,
assume h: kkernel f,
assume g : G,
calc f (g * k * g⁻¹) = f (g * k) * f g⁻¹ : by rewriteis_hom f
... = f g * f k * f g⁻¹ : by rewriteis_hom f
... = f g * e * f g⁻¹ : by rewritekkernel f
... = f g * e * (f g)⁻¹ : by rewrite (is_hom.inv f)
... = e : by simplify
end

D.3.3.3. Proof B

Let kkernel f and g be an element of G. We must show f (g * k * g⁻¹) = e. Since f k = e, we have

(D.13).
f (g * k * g⁻¹) = f (g * k) * f g⁻¹
= f g * f k * f g⁻¹
= f g * e * f g⁻¹
= f g * f g⁻¹
= f (g * g⁻¹)
= f e
= e

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 : HG, and some g : G, for all kkernel 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.14).
theorem intersection_is_open {A B : set X} : is_open A → is_open B → is_open (A ∩ B) :=
begin
assume h: is_open A,
assume h: is_open B,
assume y : X,
assume h: y ∈ A ∩ B,
casesy ∈ A ∩ B›,
obtain ⟨η, η_pos, h_η⟩ : ∃ η, (η > 0) ∧ ∀ x, dist x y < η → x ∈ A,
applyis_open A›, applyy ∈ A›,
obtain ⟨θ, θ_pos, h_θ⟩ : ∃ θ, (θ > 0) ∧ ∀ x, dist x y < θ → x ∈ B,
applyis_open B›, applyy ∈ B›,
let ε := min η θ,
have ε_pos : ε > 0,
apply lt_min ‹η > 0› ‹θ > 0,
show(ε :), ε > 0 ∧ ∀ (x : X), (dist x y < ε)(x(A ∩ B)),
use [ε, ‹ε > 0],
assume x : X,
assume h: dist x y < ε,
have : dist x y < η,
calc dist x y < min η θ :dist x y < ε›
... ≤ η : min_le_left _ _,
have : dist x y < θ,
calc dist x y < min η θ :dist x y < ε›
... ≤ θ : min_le_right _ _,
show x ∈ A ∩ B,
split,
show x ∈ A,
apply h_η, applydist x y < η›,
show x ∈ B,
apply h_θ, applydist x y < θ›,
end

D.3.4.2. Proof B

Let y be an element of AB. Then yA and yB. Therefore, since A is open, there exists η > 0 such that xA whenever dist x y < η and since B is open, there exists θ > 0 such that xB whenever dist x y < θ. We must choose ε > 0 such that xAB 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)].

Suppose A and B are both open. Let yAB . Since A is open, there is η > 0 with dist x y < ηxA for all x. Also, since B is open, there is θ > 0 with dist x y < θxB for all x. Therefore, if ε is the minimum of η and θ , then we have xAB whenever dist x y < ε for all x. So AB 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.

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, DexterCambridge Notes (2018)view onlineGitHub: https://github.com/dalcde/cam-notes
  • [Edg07]Edgar, GeraldMeasure, topology, and fractal geometry (2007)publisher Springer Science and Business Media
© 2021 E.W.Ayers. Built with Gatsby