Kevin's talk at Big Proof

Stream: general

[Scott Morrison]

I've just uploaded Kevin's talk at the Big Proof meeting at Edinburgh.

[Kevin Buzzard]

http://wwwf.imperial.ac.uk/~buzzard/docs/buzzard_big_proof2019.pdf

[Keeley Hoek]

What if there was a theorem prover where whenever you declared a structure, unless you explicitly declared that you wouldn't (with the evil keyword or something :D), you had to provide a notion of isomorphism, and it was then illegal to make a definition which used the structure without that definition being transportable over under your defined notion of isomorphism?

[Johan Commelin]

Isn't that more or less HoTT?

[Keeley Hoek]

I have no idea

[Johan Commelin]

HoTT even figures out the notion of isomorphism for you

[Keeley Hoek]

hmm. I don't know anything about HoTT. But that world seems scary---and for some reason spheres are different!

I just want is_local R to have an (autogenerated) proof that it is preserved by ring isomorphism!!

[Keeley Hoek]

I just love the aesthetic of evil def dagger_category := ...

[Mario Carneiro]

@Kevin Buzzard Here's your missing M1F problem:

import set_theory.zfc

namespace Set

def of_nat : ℕ → Set
| 0     := ∅
| (n+1) := insert (of_nat n) (of_nat n)

instance : has_coe ℕ Set := ⟨of_nat⟩

theorem omega_nat : ∀ n : ℕ, ↑n ∈ omega
| 0     := omega_zero
| (n+1) := omega_succ (omega_nat n)

theorem singleton_subset {a b : Set} : {a} ⊆ b ↔ a ∈ b :=
⟨λ h, h (mem_singleton.2 rfl), λ H c h, ((@mem_singleton c a).1 h).symm ▸ H⟩

theorem ne_empty_of_mem {a b : Set} (h : a ∈ b) : b ≠ ∅ :=
λ h0, Set.mem_empty a (h0 ▸ h)

theorem insert_ne_empty (a b : Set) : insert a b ≠ ∅ :=
ne_empty_of_mem $ mem_insert.2 $ or.inl rfl

theorem succ_ne_empty (n : ℕ) : (↑(n+1:ℕ) : Set) ≠ ∅ := insert_ne_empty _ _

end Set
open Set

def X : Set.{0} := {↑1, ↑2, {↑2}, {↑1, ↑2}}

theorem two_mem_X : ↑2 ∈ X :=
mem_insert.2 $ or.inr $ mem_insert.2 $ or.inr $ mem_insert.2 $ or.inl rfl

example : {↑2} ∈ X := mem_insert.2 $ or.inr $ mem_insert.2 $ or.inl rfl

example : {↑2} ⊆ X := singleton_subset.2 two_mem_X

example : ¬ ↑2 ⊆ X := begin
  intro h,
  replace h := @h ∅ (show ↑0 ∈ {↑0, ↑1}, from mem_insert.2 $ or.inr $ mem_singleton.2 rfl),
  rw [X] at h,
  rcases mem_insert.1 h with e | h, exact (insert_ne_empty _ _) e.symm,
  rcases mem_insert.1 h with e | h, exact (insert_ne_empty _ _) e.symm,
  rcases mem_insert.1 h with e | h, exact (succ_ne_empty _) e.symm,
  rcases mem_insert.1 h with e | h, exact (succ_ne_empty _) e.symm,
  exact mem_empty _ h
end

[Mario Carneiro]

I originally wrote lists to help solve this problem, but ZFC set theory approach works too. With lists the whole thing is decidable so you could just use dec_trivial for everything

[Kenny Lau]

don't we have $V_\omega$ in mathlib or something

[Mario Carneiro]

yeah, that's lists, more or less

[Mario Carneiro]

it's actually finite ZFA

[Mario Carneiro]

so X here is a member of lists nat where the nat gives atoms at the bottom like 1 and 2. Here I used finite von Neumann ordinals for 1 and 2 and so the final part is a bit tricky since you have to show that the empty set is not equal to 1 or 2

[Scott Morrison]

What if there was a theorem prover where whenever you declared a structure, unless you explicitly declared that you wouldn't (with the evil keyword or something :D), you had to provide a notion of isomorphism, and it was then illegal to make a definition which used the structure without that definition being transportable over under your defined notion of isomorphism?

I think this is just a matter of not ever writing def my_predicate (X : Type) [group X] : Prop := ..., and instead writing def my_predicate_functorial (G : core Group) ⥤ Prop := ....

One then hopes that the map field of the functor can be built by automation. Once that automation is in place, one goes back to just writing
def my_predicate (X : Type) [group X] : Prop := ..., but with @[derive iso_functorial] prepended, and then you have transport of structure using the tactic iso_induction Yiming is writing.

[Keeley Hoek]

isodef my_predicate (X : Type) [group X] : Prop := ...

[Johan Commelin]

The difference between @[derive iso_functorial] def and isodef is not too big... I could handle that.

[Johan Commelin]

We (read: Mario and Floris) solved Larry's challenge in 3 days. Let's see what the other communities can do with Kevin's challenges (-;

[Kevin Buzzard]

I had a long talk to Larry Paulson after my talk. He was interested in how it all happened. Someone (I forgot who :-( ) told me that they were very sorry to lose Floris! Maybe they were from Nijmegen? Maybe it was Freek.

I am leaving Big Proof now :-/ I have a talk to give in London tomorrow and I also need to get back to Imperial because I have an unformalisation project to supervise! The project is to take data.filter.basic and translate it into pdf form :-) Patrick told me that he didn't know a good reference for this stuff.

[Johan Commelin]

Wow! unformalisation. That sounds like we're living the future.

[Kevin Buzzard]

I don't know how many Lean people there were at Big Proof 2017, but I really felt that we were the dominant tribe in Big Proof 2019. There was me, Sander Dahmen, Rob Lewis, Patrick Massot, Neil Strickland, Ed Ayers, Jeremy Avigad, Scott Morrison, and also all the people I've forgotten because I'm a fool. On the Isabelle side there was Larry Paulson, his post-docs Angeliki Koutsoukou Argyraki and Wenda Li, and Manuel Eberl and Mohammad Abdulaziz from Munich, and then representing other systems we had Peter Koepke and John Harrison (who I'd never met before and who is a really nice guy). I'm trying to list all the people who were into formalising mathematics; I have probably forgotten some people; I'll edit if I've made any real howlers.

I found it very interesting talking to the Isabelle people.

[Kevin Buzzard]

Wojciech Nawrocki was also there.

[Johan Commelin]

I'm proof reading the print proofs of one of my papers, and I realised that it has a nice example of the mathematicians code of honour:

• Definition 1.a: two gadgets X and Y are called quasi-compatible if blah...
• Definition 1.b: two gadgets X and Y are called strongly quasi-compatible if blah... and bleh...
• Remark: :warning: it is not known whether strong quasi-compatibility is an equivalence relation.

[Johan Commelin]

I don't spend a word on whether quasi-compatibility is an equivalence relation. And the warning/remark was only added after Deligne pointed out to me that I should add the warning. :grinning_face_with_smiling_eyes:

[Floris van Doorn]

@Kevin Buzzard Yeah, I did my master thesis under supervision of Freek, so it was probably him.

@Scott Morrison Thanks for the nice video of the talk! And great talk as always, Kevin!

@Johan Commelin I've also done some unformalization of HoTT proofs, where the formal proof existed before it was written up anywhere.

[David Michael Roberts]

What if there was a theorem prover where whenever you declared a structure, unless you explicitly declared that you wouldn't (with the evil keyword or something :D), you had to provide a notion of isomorphism, and it was then illegal to make a definition which used the structure without that definition being transportable over under your defined notion of isomorphism?

Something based on Bourbaki's set theory? That would be evil.

[Kevin Buzzard]

https://xenaproject.wordpress.com/2019/06/02/equality-part-3-canonical-isomorphism/

@David Michael Roberts grilled me on Twitter a bit about my claims about equality and how it's confused with canonical isomorphism by even the greatest mathematicians. I wrote some more about this on my blog, stuff which didn't make it into the talk.

The more I think about canonical isomorphism, the more I realise how impossible it is to make a tactic which does everything a mathematician does with it -- not least because some stuff we do with it is really quite subtle.

[Johan Commelin]

@Kevin Buzzard Here are some marvellous code snippets to kickstart your week: https://github.com/leanprover-community/mathlib/search?q=canonical&unscoped_q=canonical

[Reid Barton]

32uczu.jpg