Who am I?

• Postdoc in number theory / arithmetic geometry
• Have worked a lot in the past on the LMFDB, website and data, a "traditional" database of mathematical objects
• Lots of computational work designing and implementing algorithms in Sage, underlying C and assembly libraries, Julia, ...
• Few years ago got interested in how proof assistants might let us write mathematical code with less bugs, or even write the description of an algorithm and the proof of correctness all together.

This talk

From the workshop website:

... data sets throughout mathematics, new database related issues arise, such as accessibility and searchability, long-term storage and stable referencing, collaborations, contributions and quality control, as well as the interlinking of data, also with other databases and computer algebra systems.

Like Kevin I'll talk about Lean and mathlib projects specifically, but with a focus on the contribution workflow how we ensure quality.

I'll talk about several tools and infrastructure, developed by the community, but some particular credit for tooling and CI belongs to, Floris van Doorn, Gabriel Ebner, Bryan Gin-Ge Chen, Robert Lewis, Scott Morrison, Eric Wieser. [1].

The case for automating proof quality checkers

• In many databases, once an algorithm is designed to generate data, more can be generated as required (with enough $$ and time)

• Person power is a limiting factor for expanding databases / libraries of proofs

• For nLab / OEIS / Wikipedia the barrier to entry is lower than for mathlib, no need to learn a new language to contribute, doesn't matter if there are small spelling / grammar mistakes (quick turnaround)

• Generating proofs automatically is very hard

• Checking / analysing existing statements and proofs is a lot easier, so we can relieve pressure on the reviewers there

What is quality for a formalized statement or proof?

Even if proofs are correct they may be less useful than expected:

• A theorem could be unnecessarily specific and therefore less helpful to others / harder to find by automated tools
• Theorems with unnecessary hypotheses place a burden on those using them to prove these side conditions, even if they do hold
• Proofs can be unnecessarily complicated, simpler proofs are easier to understand (for both humans and computers!), easier fix when they break, and easier generalize / copy to different contexts.
• Any theorem with contradictory or false hypotheses will be provable, but likely useless not what was intended unless the conclusion is actually a contradiction!

Can occur due to the collaborative and revisionary nature of the project, most proofs are not written once and set in stone, but revised often by different authors, this can lead to oversights and inconsistencies. Some of these issues are caught by human reviewers when the results are added to the library, sometimes not.

Eventually we would love proof assistants to be genuinely helpful assistants when working on mathematics, in addition to simply checking that we haven't made mistakes, if they could also suggest genuine improvements.

Mathlib Continuous Integration (CI)

In the mathlib library:

• Continuous integration is run on every commit
• It can take up to 5 hours in the worst case, if a basic file is modified as it involves:
  • Checking the proofs
  • Caching a low level version for download so others don't have to check the entire library on their computer
  • Running linters to catch common mistakes, and ensure documentation is added
  • Basic syntax / formatting linting to make the source files more uniform (makes searching by text more effective)

People can (and do) make small contributions from the web browser, making changes via the github interface or gitpod, and letting CI find what broke and the location of the error.

Speeding up CI

In order for CI to be as fast as possible it is important that any files that don't need to be rebuilt are not. To do this we have to ensure files don't import things they don't need.

Me and Johan Commelin wrote a tool (in Lean) to inspect Lean files and print only the imports that are actually needed from the ~2200 files.

Anatomy of a proof

Proofs are written in an interactive style using commands (tactics) such as

• by_cases - to split into cases based on some hypothesis holding or its negation
• use - to pick a witness of an existential statement
• rewrite - to substitute some known equality in
• contrapose
• contradiction
• linarith - prove statements involving linear inequalities on reals
• ring - prove ring theoretic identities completely customisable, aim to represent a logical step in a somewhat human level, source code

In the process of checking they are converted into a low level format (compiled code) of expressions that consists only of the primitive pieces:

• A reference to another definition or statement in the library, nat.even
• An (partial) application of a function to some argument, nat.even 2
• An anonymous function, λ x, x + 1
• The type of all functions from one type to another
• Let x = blah in the following

Can think of this as a tree of subexpressions $$a_i={\int }_{\sqrt{\frac{a-b}{2}}}^{\sqrt{\frac{a+b}{2}}}{x}^{2}dx$$

By iterating over such trees we can study compiled proofs after the fact, and find and suggest improvements, this is what is done in CI, not studying the source.

Unused assumptions

In the following

lemma add_one_sq {R : Type*} [comm_ring R] [is_domain R] (r : R) :
  (r + 1) ^ 2 = r ^ 2 + 2 * r + 1 :=
begin
  simp [mul_add, add_mul],
  abel,
end

The fact [is_domain R] is never used in the proof!

In the tree of expressions generated for the proof we will see that the assumption [is_domain R] never appears by name, and is therefore removable.

This is actually quite common, when working on a long file we normally set the assumptions at the top, and leave them for a whole section. Its easy on paper and in Lean to neglect to think back on what the working hypothesis for some section is.

Duplicate lemmas

Lemmas can be duplicates of each other with different proofs, most of the time this is unintentional, leads to fragmentation and missed opportunities for improvements.

By hashing the types of lemmas and throwing them into a dictionary we can quickly find these. Being a bit smarter we can hash up to common variations, such as rearranging the arguments.

There more than 100 pairs of duplicates in mathlib last time I checked, many due to copy-paste errors:

lemma differentiable_at_cosh {x : ℂ} : differentiable_at ℂ cos x :=
differentiable_cos x

Requires an inhumanly detailed reviewer to catch something like this in PR review!

Unnecessary case splits

Similarly if we make use of a case split in a proof, but then don't use one of the new hypothesis we didn't need to split into cases originally:

lemma uniformly_extend_spec {α β γ : Type*} [uniform_space α] [uniform_space β] [uniform_space γ]
  {e : β → α} (h_e : uniform_inducing e) (h_dense : dense_range e) {f : β → γ}
  (h_f : uniform_continuous f) [separated_space γ] [complete_space γ] (a : α) :
  tendsto f (comap e (𝓝 a)) (𝓝 (ψ a)) :=
let de := (h_e.dense_inducing h_dense) in
begin
  by_cases ha : a ∈ range e,
  { rcases ha with ⟨b, rfl⟩,
    rw [uniformly_extend_of_ind _ _ h_f, ← de.nhds_eq_comap],
    exact h_f.continuous.tendsto _ },
  { simp only [dense_inducing.extend, dif_neg ha],
    exact tendsto_nhds_lim (uniformly_extend_exists h_e h_dense h_f _) }
end

in this example ha is only used in the first branch, and when we remove the split, it turns out the hypothesis [separated_space γ] is no longer needed. The proof becomes

by simpa only [dense_inducing.extend] using tendsto_nhds_lim (uniformly_extend_exists h_e ‹_› h_f _)

and we can consequently remove the separated_space assumption from 10 other lemmas in the library.

We just avoided someone potentially having to do this by hand later.

Generalizing (typeclass) assumptions

Problem: Often theorems are stated with stronger, but still used, typeclass assumptions than are really needed, can this be detected automatically?

A fake Lean lemma:

lemma mul_inv {G : Type*} [ordered_comm_group G] (a b : G) : (a * b)⁻¹ = a⁻¹ * b⁻¹ :=
by rw [mul_inv_rev, mul_comm]

This assumes [ordered_comm_group G] but makes no mention of an order! In principle the proof could still require it, but it doesn't.

Anyone trying to use this theorem for a comm_group G would get an error!

The "correct" assumption is [comm_group G], when this is changed the proof script does not need modifying.

A real lemma from mathlib:

lemma ring_hom.char_p_iff_char_p {K L : Type*} [field K] [field L]
  (f : K →+* L) (p : ℕ) : char_p K p ↔ char_p L p :=
begin
  split;
  { introI _c, constructor, intro n,
    rw [← @char_p.cast_eq_zero_iff _ _ p _c n, ← f.injective.eq_iff, f.map_nat_cast, f.map_zero] }
end

Correct assumptions: [division_ring K] [nontrivial L] [semiring L]

How do typeclasses work?

Lean automatically generates the terms used in the proof:

@ordered_comm_group.to_ordered_cancel_comm_monoid G _inst_1
@ordered_cancel_comm_monoid.to_ordered_comm_monoid ...
@ordered_comm_group.to_comm_group G _inst_1
...

via typeclass resolution. The following instances appear in the proof term:

It is possible to determine after the fact what the real assumptions needed are by finding least common anscestors in a large graph of possibilities.

The graph of all these structures is rather big

See https://observablehq.com/@alexjbest2/lean-generalisation for a (small) sample:

(*) Only terms reachable from linear_ordered_field here, generated Jan 2021, it has grown since then!

Example output:

/- The `generalisation_linter` linter reports: -/
/- typeclass generalisations may be possible -/
-- topology\algebra\group.lean
#print nhds_translation_mul_inv /- _inst_3: topological_group ↝ has_continuous_mul
 -/
#print nhds_translation_add_neg /- _inst_3: topological_add_group ↝ has_continuous_add
 -/
#print quotient_add_group.is_open_map_coe /- _inst_3: topological_add_group ↝ has_continuous_add
 -/
#print quotient_group.is_open_map_coe /- _inst_3: topological_group ↝ has_continuous_mul
 -/
#print is_open.add_left /- _inst_3: topological_add_group ↝ has_continuous_add
 -/
#print is_open.mul_left /- _inst_3: topological_group ↝ has_continuous_mul
 -/
#print is_open.add_right /- _inst_3: topological_add_group ↝ has_continuous_add
 -/
#print is_open.mul_right /- _inst_3: topological_group ↝ has_continuous_mul
 -/
#print topological_group.t1_space /- _inst_3: topological_group ↝ has_continuous_mul
 -/
#print compact_open_separated_mul /- _inst_3: topological_group ↝ has_continuous_mul
 -/
#print compact_open_separated_add /- _inst_3: topological_add_group ↝ has_continuous_add
 -/
#print compact_covered_by_mul_left_translates /- _inst_3: topological_group ↝ has_continuous_mul
 -/
#print compact_covered_by_add_left_translates /- _inst_3: topological_add_group ↝ has_continuous_add
 -/

This is naturally an iterative process: once the assumptions lemmas are changed dependent declarations may become generalizable.

• The current implementation is fast enough for interactive use.
• Alternative would be to transform declarations in place when working through the environment

Some common replacements in mathlib

Running a single pass of this on my laptop on the 80,000 declarations in mathlib finished overnight.

Connections with other databases

A proof assistant can be used to write code that is proven to compute what is intended correctly

This can be used in several stages of the "traditional" mathematical database pipeline:

• Data generation
• Data update / modification
• Tracking range / completeness of database (complicated constraints)
• Display of the data, provably correct printing
• Using known results to optimize searches

Why not try to write your next update script in Lean? (other ITPs are available) This is hard without a library that understands the objects you are studying rigorously.

Removable edge cases

So far we have talked a lot about simplifying proofs, what about simplifying statements?

One common and annoying way statements can be sub-optimal is that they have conditions about edge cases that need verifying. This is one of the things that makes formal proof more time consuming than informal proof.

The following is an example of a statement about a group G.

lemma exponent_dvd_of_forall_pow_eq_one (n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) :
  exponent G ∣ n :=
begin
  apply nat.dvd_of_mod_eq_zero,
  by_contradiction h,
  have h₁ := nat.pos_of_ne_zero h,
  have h₂ : n % exponent G < exponent G := nat.mod_lt _ (exponent_pos_of_exists _ n hpos hG),
  have h₃ : exponent G ≤ n % exponent G,
  { apply exponent_min' _ _ h₁,
    simp_rw ←pow_eq_mod_exponent,
    exact hG },
  linarith,
end

By changing the type from

lemma exponent_dvd_of_forall_pow_eq_one (n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) : exponent G ∣ n

to

lemma exponent_dvd_of_forall_pow_eq_one (n : ℕ) (hG : ∀ g : G, g ^ n = 1) : exponent G ∣ n

the whole first half of the following proof in the same file becomes unnecessary:

lemma lcm_order_eq_exponent {H : Type*} [fintype H] [left_cancel_monoid H] :
  (finset.univ : finset H).lcm order_of = exponent H :=
begin
  apply nat.dvd_antisymm (lcm_order_of_dvd_exponent H),
  apply exponent_dvd_of_forall_pow_eq_one,
  { apply nat.pos_of_ne_zero,
    by_contradiction,
    rw finset.lcm_eq_zero_iff at h,
    cases h with g hg,
    simp only [true_and, set.mem_univ, finset.coe_univ] at hg,
    exact ne_of_gt (order_of_pos g) hg },
  { intro g,
    have h : (order_of g) ∣ (finset.univ : finset H).lcm order_of,
    { apply finset.dvd_lcm,
      exact finset.mem_univ g },
    cases h with m hm,
    rw [hm, pow_mul, pow_order_of_eq_one, one_pow] },
end

Unused haves / suffices

If we have a proof using

have h : some_fact := <proof_of_fact>,
<rest_of_proof>

or

suffices h : some_fact,
<rest_of_proof>,
<proof_of_fact>

and where rest_of_proof doesn't make use of the hypothesis h, then introducing and proving h in this way was unnecessary. From the perspective of the expression trees this is a branch that doesn't refer to some variable.

Such as

lemma mem_traverse {f : α' → set β'} :
  ∀(l : list α') (n : list β'), n ∈ traverse f l ↔ forall₂ (λb a, b ∈ f a) n l
| []      []      := by simp
| (a::as) []      := by simp; exact assume h, match h with end
| []      (b::bs) := by simp
| (a::as) (b::bs) :=
  suffices (b :: bs : list β') ∈ traverse f (a :: as) ↔ b ∈ f a ∧ bs ∈ traverse f as,
    by simp [mem_traverse as bs],
  iff.intro
    (assume ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩, ⟨hb, hl⟩)
    (assume ⟨hb, hl⟩, ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩)

can become

lemma mem_traverse {f : α' → set β'} :
  ∀(l : list α') (n : list β'), n ∈ traverse f l ↔ forall₂ (λb a, b ∈ f a) n l
| []      []      := by simp
| (a::as) []      := by simp
| []      (b::bs) := by simp
| (a::as) (b::bs) := by simp [mem_traverse as bs]