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:

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;

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
  obtain ⟨x, 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 h₂ 1
        ...  = 4     : by norm_num
end

D.2.5. Reference table for tactics

Table D.4
Table D.5

Table D.4 continued.

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.6)
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


(g ∘ f) x := g (f (x))

D.3.1.2. Proof A

(D.7)
theorem hom_composition : is_hom f → is_hom g → is_hom (g ∘ f) :=
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 : 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

(D.8)
(g ∘ f)(x * y) = g(f(x * y))
               = g(f(x) * f(y))
               = g(f(x)) * g(f(y))
               = (g ∘ f)(x) * g(f(y))
               = (g ∘ f)(x) * (g ∘ f)(y)

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

(D.9)
(g ∘ f)(x * y) = g(f(x * y))
               = g(f(x) * f(y))
               = g(f(x)) * g(f(y))
               = (g ∘ f)(x) * (g ∘ f)(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.10)
dist : X → X → ℝ

such that the following properties hold:

We say a subset A : set X is open when

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

D.3.2.2. Proof A

(D.12)
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,
  cases ‹y ∈ A ∪ B›,
  { -- in the case that y ∈ A
    obtain ⟨η, η_pos, h₄⟩ : ∃ η, (η > 0) ∧ ∀ x, dist x y < η → x ∈ A,
    { apply ‹is_open A›,
      apply ‹y ∈ A›,
    },
    show ∃ ε, (ε > 0) ∧ ∀ x, dist x y < ε → x ∈ A ∪ B,
    use [η, η_pos],
    show ∀ x, 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,
    { apply ‹is_open B›,
      apply ‹y ∈ 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 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.13)
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.14)
theorem kernel_is_normal : is_normal (kernel f) :=
begin
  assume k : G,
  assume h₁ : k ∈ kernel f,
  assume g : G,
  calc f (g * k * g⁻¹) = f (g * k) * f g⁻¹ : by rewrite ‹is_hom f›
                   ... = f g * f k * f g⁻¹ : by rewrite ‹is_hom f›
                   ... = f g * e * f g⁻¹   : by rewrite ‹k ∈ kernel f›
                   ... = f g * e * (f g)⁻¹ : by rewrite (is_hom.inv f)
                   ... = e                 : by simplify
end

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

(D.15)
 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 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.1. Proof A

(D.16)
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,
  cases ‹y ∈ A ∩ B›,
  obtain ⟨η, η_pos, h_η⟩ : ∃ η, (η > 0) ∧ ∀ x, dist x y < η → x ∈ A,
    apply ‹is_open A›, apply ‹y ∈ A›,
  obtain ⟨θ, θ_pos, h_θ⟩ : ∃ θ, (θ > 0) ∧ ∀ x, dist x y < θ → x ∈ B,
    apply ‹is_open B›, apply ‹y ∈ 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_η, apply ‹dist x y < η›,
  show x ∈ B,
    apply h_θ, apply ‹dist x y < θ›,
end

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:

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.

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)https://dec41.user.srcf.net/notesGitHub: https://github.com/dalcde/cam-notes
  • [Edg07]Edgar, GeraldMeasure, topology, and fractal geometry (2007)publisher Springer