100 theorems

Stream: general

[Floris van Doorn]

I'm updating the 100 theorems for Lean: https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md
for Freek's 100 theorem project: http://www.cs.ru.nl/~freek/100/

Who should I cite as the author for De Moivre's Theorem?

• Abhimanyu Pallavi Sudhir, who did the actual theorem (link)
• Chris Hughes, who did (or at least committed) all the work, so that the theorem could be proven in a few lines
• or mathlib

[Floris van Doorn]

I'm going through Mario's list. I don't think we have Brouwer's fixed point theorem. I can only find the Banach fixed point theorem: https://github.com/leanprover-community/mathlib/blob/f25340175631cdc85ad768a262433f968d0d6450/src/topology/metric_space/lipschitz.lean#L110

[Floris van Doorn]

Do we have Bezout's theorem in mathlib? The closest I can find is https://github.com/leanprover-community/mathlib/blob/78f1949719676db358ea5e68e211a73e2ce95e7b/src/data/int/modeq.lean#L107

[Neil Strickland]

I don't think we can do the Brouwer fixed point theorem without knowing either \pi_n or H_n of the n-sphere. (Either one would do, but H_n would be tidier.) It looks like @Reid Barton has defined \pi_n but we don't have any calculations and we don't have H_n.

[Floris van Doorn]

We had the number of combinations in Lean 2: https://github.com/leanprover/lean2/blob/227fcad22ab2bc27bb7471be7911075d101ba3f9/library/theories/combinatorics/choose.lean#L208
I don't think it's in Lean 3 yet. Someone port this! :)

[Neil Strickland]

That's card_powerset_len at https://github.com/leanprover-community/mathlib/blob/00aaf05a00b928ea9ac09721d87ae5d2ca1ae5a1/src/data/finset.lean#L1300

[Floris van Doorn]

Thanks!

[Floris van Doorn]

Ah, when searching for the Euclidean Algorithm, I found Bezout's theorem:
https://github.com/leanprover-community/mathlib/blob/4845b663c182704738868db5861ffb4c6056be23/src/algebra/euclidean_domain.lean#L233

[Kevin Buzzard]

72. Sylow’s Theorem

What even is Sylow's Theorem? Chris proved all three Sylow Theorems as part of his 1st year project last year: https://github.com/ChrisHughes24/Sylow . The things I was told were Sylow's theorems are all pretty near the bottom of the file.

[Floris van Doorn]

What should I cite as the Euclidean Algorithm? Maybe just the definition of gcd?

def gcd : α → α → α
| a := λ b, if a0 : a = 0 then b else
  have h:_ := mod_lt b a0,
  gcd (b%a) a
using_well_founded {dec_tac := tactic.assumption,
  rel_tac := λ _ _, `[exact ⟨_, r_well_founded α⟩]}

[Floris van Doorn]

@Kevin Buzzard I think these three theorems: https://en.wikipedia.org/wiki/Sylow_theorems

I saw the first one at the bottom of the sylow.lean file in mathlib, and therefore assumed that the other 2 were not yet proven, but I'll dig a little deeper.

[Neil Strickland]

The Isabelle version proves only the existence of Sylow p-subgroups, which is what we have in mathlib. HOL Light, Metamath, Coq and Mizar all have the other theorems: all Sylow subgroups are conjugate, and their number is congruent to one mod p and divides the order of the group. These also appear in Chris's repository, and should certainly move into mathlib at some point.

[Kevin Buzzard]

I don't know what made it into mathlib; my post linked to the repo Chris wrote for his project. I'm assuming we can link to non-mathlib stuff?

[Floris van Doorn]

Of course! I'll link to that repository.

[Chris Hughes]

I should PR the other two theorems at some point. Haven't done it yet.

[Floris van Doorn]

Did you formalize the last part of Theorem 3?

np = |G : NG(P)|, where P is any Sylow p-subgroup of G and NG denotes the normalizer.

[Floris van Doorn]

Should I cite Leo de Moura author of The Principle of Mathematical Induction in Lean? :P

[Floris van Doorn]

Have we proven that int is a unique_factorization_domain?

[Chris Hughes]

We have proven that int is a UFD. This is probably multiple authors, because it goes via general results about Euclidean domains and PIDs. But mainly Johannes. It's there for nat as well, and that was Mario.

[Neil Strickland]

In algebra.euclidean_domain we have int.euclidean_domain. In ring_theory.principal_ideal_domain we have euclidean_domain.to_principal_ideal_domain and principal_ideal_domain.to_unique_factorization_domain.

[Floris van Doorn]

Ah, thanks!

[Floris van Doorn]

I'll use mathlib as the author.

[Chris Hughes]

I don't think I formalised that last part of theorem three. I don't understand your statement.

[Floris van Doorn]

Ok. It's the last bullet point of Theorem 3 from Wikipedia: https://en.wikipedia.org/wiki/Sylow_theorems

[Neil Strickland]

But principal_ideal_domain.to_unique_factorization_domain is not an instance, so by apply_instance : unique_factorization_domain ℤ fails. I'm not sure why that is. It might be related to the fact that principal_ideal_domain.to_unique_factorization_domain is marked as noncomputable.

[Chris Hughes]

It is because of that fact.

[Neil Strickland]

That bullet point is the have at line 935 of https://github.com/ChrisHughes24/Sylow/blob/master/src/sylow.lean, but it is not stated as a separate theorem.

[Floris van Doorn]

Ah, ok. Then I'll just write that.

[Rob Lewis]

I can claim an earlier proof of the IVT, although I'm not sure we want to draw anyone's attention to the days before simp and style conventions! https://github.com/leanprover/lean2/blob/master/library/theories/analysis/ivt.lean

[Floris van Doorn]

I updated the markdown file. We have formalized 23/100 results (that I could find).

[Floris van Doorn]

https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md

[Floris van Doorn]

The ones on Mario's list that I couldn't find:

• 78 (cauchy-schwarz)
• 94 (law of cosines)

[Floris van Doorn]

In cases that there is not a clear single author, I now liberally used mathlib as an author. If anyone is unhappy with that, feel free to change it.

[Chris Hughes]

I don't think I should be the author of Bezout's theorem. I more or less copied that proof exactly from the nat version.

[Floris van Doorn]

Ok, I'll change it to mathlib.

I used Github's history to figure out authorship. This is of course a flawed method. Please check if there are attributions which are clearly wrong.

[Floris van Doorn]

I emailed Freek to point him to the markdown file (Lean now looks so sad with a score of 1 on his page).

[Neil Strickland]

At http://bim.shef.ac.uk/lean/hundred_theorems.html I put a crude analysis of what would be needed for the remaining theorems.

[Mario Carneiro]

I think both law of cosines and cauchy schwarz are "in the air" at this point, i.e. someone just has to actually write down and prove the statement

[Mario Carneiro]

for law of cosines, I'm not quite sure how to do it in a general vector space without it being tautological

[Kenny Lau]

I thought 6. Godel's Incompleteness Theorem was already done?

[Mario Carneiro]

certainly not. I think isabelle has the only known proof

[Mario Carneiro]

oh, Freek says there are also others

[Mario Carneiro]

but it's one of the "hard problems" on the list

[Mario Carneiro]

you have to build proof theory first

[Kenny Lau]

I thought someone proved it in the conference we went to

[Kenny Lau]

I remember the independence of continuum hypothesis having been proved

[Kenny Lau]

so there is definitely a proof theory

[Mario Carneiro]

That's true, Floris and Jesse are soon to be the first to do the independence of the continuum hypothesis, and they had to build a proof theory for that

[Mario Carneiro]

but they didn't do anything with arithmetization (although I did, for computability stuff)

[Mario Carneiro]

you still have to do quite a lot of work in the embedded proof theory (basically PA), and we're slowly learning how to do that without tearing our hair out

[Scott Morrison]

@Martin Skilleter has the Cauchy-Schwarz inequality.

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md#86-lebesgue-measure-and-integration is misleading. This is not Lebesgue integral.

[Mario Carneiro]

I don't think it is. It's less than we want from our integration library, but it's definitely the lebesgue measure and the integral on that measure

[Mario Carneiro]

if anything, the problem with this challenge in general is that there's no clear theorem or definition to point to

[Mario Carneiro]

it's really a statement about a whole construction

[Keeley Hoek]

Perhaps a link to the "main" file?

[David Michael Roberts]

That's true, Floris and Jesse are soon to be the first to do the independence of the continuum hypothesis, and they had to build a proof theory for that

So where is the constructible universe up to (or are they using the hierarchy that uses HOD instead of L?)

[Mario Carneiro]

I don't think they are planning on doing L, actually. Jesse says there is a way to do it with forcing, which will be nice if true since they already had to build all that for the first part (proving that CH is unprovable)

[David Michael Roberts]

Oh, I see, collapsing P(N) to aleph_1. Nice.

[David Michael Roberts]

"Just" construct the correct boolean algebra and turn the handle to get new model of ZFC, and then show CH is true therein. :-)

[Floris van Doorn]

@Martin Skilleter If you give a link to your formalization of the Cauchy-Schwarz inequality, I will link to it.

[Floris van Doorn]

@Patrick Massot What is missing from the definition of the Lebesgue integral? I'm happy to remove if something is missing. I agree with Mario that the challenge is stupid because it asks for a definition, not the proof of a theorem.

[Mario Carneiro]

One reasonable argument you can levy against our integral is that it doesn't support functions R -> R

[Mario Carneiro]

to which we say "Bochner integral is coming" and by then we've already shot right past the conventional definition

[Floris van Doorn]

@Neil Strickland Nice list! Doing the Arithmetic Mean/Geometric Mean should be a small project if done directly (there is a pretty easy induction argument, which shows that if the inequality holds for n then it holds for 2n and n-1), but what we probably want is to show that the Power mean is an increasing function.

[Floris van Doorn]

@Mario Carneiro Oh, that's fair. Do you think that is big enough of an omission to remove it from the list?

[Mario Carneiro]

I don't, as I said to Patrick. I think that we've done all the important stuff that pertains to lebesgue integral already. In the future when we have Bochner integral and are asked to identify where is the Lebesgue integral, we will still point to the ennreal definition

[Reid Barton]

I have (23) Formula for Pythagorean Triples on my old laptop. It was part of my first real Lean project.
I can try updating it to modern mathlib when I get home.

[Reid Barton]

A year later, I'm still not sure what the mathlib-approved way to talk about even and odd numbers is.

[Alex J. Best]

I just finished having a go at one of these, every prime congruent to 1 mod 4 is a sum of two squares (@Chris Hughes has already done it, but my version is quite... different). I tried to formalise Don Zagier's (in)famous one-sentence proof https://people.mpim-bonn.mpg.de/zagier/files/doi/10.2307/2323918/fulltext.pdf it turned out to be a few more than 1 sentence of course, but I stuck pretty much exactly to the intended argument.

I'd appreciate any comments people have (especially on how to break it up into separate lemmas, or reduce its size, in the course of the proof it has turned into one giant, semi-impossible-to-compile monolith so. I tried but sort of gave up on shrinking it now). I'm pretty sure it compiles, but my computer times out if I try and do it all in one go.
This was the first big project I've tried so fair to say, I learned a lot!

https://gist.github.com/alexjbest/1fcc06a67f4d56275f99c44037bb1b6d

[Johan Commelin]

Wow, that's almost 500 lines of proof!

[Kevin Buzzard]

The timeout might not be because of your computer -- it might be a more serious problem.

[Kevin Buzzard]

oh wait -- I can get it to compile from the command line. so I think it's OK! Well done!

[Alex J. Best]

Oh its definitely a serious problem, I didn't mean to imply that it wasn't! But probably there is a solution I'm not aware of, every time I tried to break it up into lemmas it all broke as everything depends on p is all.

[Kevin Buzzard]

wait, I spoke too soon :-/

[Kevin Buzzard]

prime.lean:614:0: error: invalid assertv tactic, value has type
  ↥fixp_j
but is expected to have type
  fixp_j
state:
p : ℕ,
pprime : nat.prime p,
p1mod4 : p % 4 = 1,
property : ℤ3 → Prop :=
  prod.rec
    (λ (fst : ℤ),
       prod.rec
         (λ (snd_fst snd_snd : ℤ),
            id_rhs Prop (fst ^ 2 + 4 * snd_fst * snd_snd = ↑p ∧ fst > 0 ∧ snd_fst > 0 ∧ snd_snd > 0))),
S : Type := subtype property,
big_set : Type := fin p × fin p × fin p,
_inst : fintype big_set,
random_func : S → big_set :=
  λ (a : S),
    subtype.cases_on a
      (λ (a_val : ℤ3) (P : property a_val),
         prod.cases_on a_val
           (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)),
              prod.cases_on a_val_snd
                (λ (Y Z : ℤ) (P : property (X, Y, Z)),
                   (⟨int.nat_abs X, _⟩, ⟨int.nat_abs Y, _⟩, ⟨int.nat_abs Z, _⟩))
                P)
           P),
random_inj : function.injective random_func,
_inst_1 : fintype S,
mainn : fintype.card S ≡ 1 [MOD 2],
j : S → S :=
  λ (a : S),
    subtype.cases_on a
      (λ (a_val : ℤ3) (P : property a_val),
         prod.cases_on a_val
           (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)),
              prod.cases_on a_val_snd (λ (Y Z : ℤ) (P : property (X, Y, Z)), ⟨(X, Z, Y), _⟩) P)
           P),
j_invo : funcpow j 2 = id,
_inst_2 : mul_action (fin 2) S := finorder_end_cyclic_action j_invo,
fixp_j : set S := fixed_points (fin 2) S,
finj : fintype ↥fixp_j,
exists_fixed_j : nonempty ↥fixp_j
⊢ ∃ (a b : ℤ), a ^ 2 + b ^ 2 = ↑p

[Kevin Buzzard]

Oh its definitely a serious problem, I didn't mean to imply that it wasn't! But probably there is a solution I'm not aware of, every time I tried to break it up into lemmas it all broke as everything depends on p is all.

This can surely be solved.

[Alex J. Best]

prime.lean:614:0: error: invalid assertv tactic, value has type
  ↥fixp_j
but is expected to have type
  fixp_j
state:
p : ℕ,
pprime : nat.prime p,
p1mod4 : p % 4 = 1,
property : ℤ3 → Prop :=
  prod.rec
    (λ (fst : ℤ),
       prod.rec
         (λ (snd_fst snd_snd : ℤ),
            id_rhs Prop (fst ^ 2 + 4 * snd_fst * snd_snd = ↑p ∧ fst > 0 ∧ snd_fst > 0 ∧ snd_snd > 0))),
S : Type := subtype property,
big_set : Type := fin p × fin p × fin p,
_inst : fintype big_set,
random_func : S → big_set :=
  λ (a : S),
    subtype.cases_on a
      (λ (a_val : ℤ3) (P : property a_val),
         prod.cases_on a_val
           (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)),
              prod.cases_on a_val_snd
                (λ (Y Z : ℤ) (P : property (X, Y, Z)),
                   (⟨int.nat_abs X, _⟩, ⟨int.nat_abs Y, _⟩, ⟨int.nat_abs Z, _⟩))
                P)
           P),
random_inj : function.injective random_func,
_inst_1 : fintype S,
mainn : fintype.card S ≡ 1 [MOD 2],
j : S → S :=
  λ (a : S),
    subtype.cases_on a
      (λ (a_val : ℤ3) (P : property a_val),
         prod.cases_on a_val
           (λ (X : ℤ) (a_val_snd : ℤ × ℤ) (P : property (X, a_val_snd)),
              prod.cases_on a_val_snd (λ (Y Z : ℤ) (P : property (X, Y, Z)), ⟨(X, Z, Y), _⟩) P)
           P),
j_invo : funcpow j 2 = id,
_inst_2 : mul_action (fin 2) S := finorder_end_cyclic_action j_invo,
fixp_j : set S := fixed_points (fin 2) S,
finj : fintype ↥fixp_j,
exists_fixed_j : nonempty ↥fixp_j
⊢ ∃ (a b : ℤ), a ^ 2 + b ^ 2 = ↑p

oh oops I broke it trying to improve readability line 614 just remove the type and it should go, I updated the gist. Thanks!

[Kevin Buzzard]

If in VS Code you do File -> Preferences -> Settings (or ctrl-,) then search for lean then scroll down until you find "Lean time limit" and change the value from 100000 to 500000 then it will remove the deterministic timeout.

[Kevin Buzzard]

You could define functions S p and bigset p etc. I'm still getting timeouts :-( There is maybe some type error somewhere, or the elaborator is going off doing something it shouldn't be doing, or something.

[Kevin Buzzard]

You must have had the patience of a saint to use Lean like this -- waiting forever for things to compile drives me nuts.

[Alex J. Best]

Yeah I ended up sorrying and commenting a lot, and having a separate scratch section for running library search and building snippets of proof up... having to do "real work" while lean is compiling wasn't the worst thing ever though

[Kevin Buzzard]

There seems to be some sort of a problem around line 569 but it's particularly obscure.

Inserting sorry, end, sorry, end #exit just after rw one_fixed_i at mainn, gets the proof compiling. However inserting end, sorry, end #exit instead, just after the next line exact mainn causes a deterministic time-out, even if the time-out variable is set to super-high (900000). We had this problem in the perfectoid project and it turned out to be a delicate issue with unification which was very hard to debug.

[Kevin Buzzard]

In short, our code was crummy in a way we had not really understood because the issue was not mathematical.

[Kevin Buzzard]

I would honestly recommend breaking up the proof into much smaller chunks so it's easier to find out what's going on. It's very frustrating to work with it as things stand.

[Kevin Buzzard]

Other comments: indent 2 spaces not 4, and indent after the initial begin so that the entire proof is two spaces in (at least).

[Alex J. Best]

Thanks, I filled in a couple more underscores there, maybe it will help a little. I think I fixed a more serious problem which was messing my lean up, lots of dsimp at *'s later on in the proof were screwing with earlier results it seems. Yet more reasons not to make one huge proof I guess.

[Alex J. Best]

I would honestly recommend breaking up the proof into much smaller chunks so it's easier to find out what's going on. It's very frustrating to work with it as things stand.

Okay I did that and it seems to work really quite well now, thanks for the recommendation

https://gist.github.com/alexjbest/1fcc06a67f4d56275f99c44037bb1b6d

I have one concrete question now, which should be easier to answer now that it compiles in seconds not minutes...

In my lemma i_invo if I delete the line unfold funcpow and let the dsimpline below unfold it looks like the proof works unchanged in the goal view, but I get a weird error message I don't understand, type mismatch at application id.. and then a lot of output. Whats going on here?

[Kevin Buzzard]

Your proof compiles fine for me now! Congratulations on proving what is quite a tricky theorem!

[Kevin Buzzard]

If I comment out unfold funcpow on line 348 the proof still compiles fine.

[Floris van Doorn]

What happened to the 100-thms branch? It doesn't exist anymore: https://github.com/leanprover-community/mathlib/tree/100-thms

[Floris van Doorn]

I pushed the branch I had locally. I don't know if we lost any commits. Is there an (automatic) cleanup of branches in mathlib?

[Johan Commelin]

I would hope there is not... I didn't backup this branch :-(

[Floris van Doorn]

I added 3. The Denumerability of the Rational Numbers and 22. The Non-Denumerability of the Continuum. Have any others been proven recently?

I'll message Freek soon to update his list.

[Kevin Buzzard]

Not all primes are the sum of two squares (number 20 title)

[Floris van Doorn]

thanks, I fixed the title.

[Johan Commelin]

@Freek Wiedijk We have 5 new items for your list:
https://github.com/leanprover-community/leanprover-community.github.io/commits/newsite/data/100.yaml

[Rob Lewis]

Hmm, but https://leanprover-community.github.io/100.html doesn't seem to have updated yet

[Floris van Doorn]

Freek just updated http://www.cs.ru.nl/~freek/100/

[Kevin Buzzard]

We're over half way there! And area of a circle is on the horizon...

[Floris van Doorn]

Yeah, there are many results that are within reach with the current state of the library. We also have open PRs for 30 (#5574) and 45 (#4259).

[Ruben Van de Velde]

Do we not have the cubic formula (37) yet? Any reason why it'd be hard?

[Kenny Lau]

I don't think it should be hard.

[Johan Commelin]

It would be good to make it general (as in, not just over the reals).

[Kevin Buzzard]

Would it? Doing it over the complexes would be easiet because all square and cube roots exist. In small characteristic there are problems (formula isn't true). Over a general field of char 0 (say) one has to decide what the statement is. There are times when the auxiliary square roots don't exist in the field and yet the cubic has a root anyway. I guess one could dodge all this by saying "the roots are this in the algebraic closure" but then you may as well be working over the complexes anyway

[Chris Hughes]

You just want the a variable and a hypothesis that they are a cube root.

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/quadratic_discriminant.lean does something like that, yeah. I think the problem is with the intermediate square roots, though

[Johan Commelin]

@Kevin Buzzard but if at some point we want to apply this, then it probably won't be over complex...