Zulip Chat Archive

Stream: general

Topic: 100 theorems


view this post on Zulip Floris van Doorn (May 29 2019 at 21:24):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 21:30):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 21:46):

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

view this post on Zulip Neil Strickland (May 29 2019 at 21:56):

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.

view this post on Zulip Floris van Doorn (May 29 2019 at 21:57):

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! :)

view this post on Zulip Neil Strickland (May 29 2019 at 22:06):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 22:12):

Thanks!

view this post on Zulip Floris van Doorn (May 29 2019 at 22:12):

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

view this post on Zulip Kevin Buzzard (May 29 2019 at 22:17):

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.

view this post on Zulip Floris van Doorn (May 29 2019 at 22:19):

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 α⟩]}

view this post on Zulip Floris van Doorn (May 29 2019 at 22:22):

@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.

view this post on Zulip Neil Strickland (May 29 2019 at 22:22):

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.

view this post on Zulip Kevin Buzzard (May 29 2019 at 22:24):

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?

view this post on Zulip Floris van Doorn (May 29 2019 at 22:25):

Of course! I'll link to that repository.

view this post on Zulip Chris Hughes (May 29 2019 at 22:28):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 22:30):

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.

view this post on Zulip Floris van Doorn (May 29 2019 at 22:34):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 22:53):

Have we proven that int is a unique_factorization_domain?

view this post on Zulip Chris Hughes (May 29 2019 at 22:59):

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.

view this post on Zulip Neil Strickland (May 29 2019 at 23:03):

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.

view this post on Zulip Floris van Doorn (May 29 2019 at 23:04):

Ah, thanks!

view this post on Zulip Floris van Doorn (May 29 2019 at 23:05):

I'll use mathlib as the author.

view this post on Zulip Chris Hughes (May 29 2019 at 23:05):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 23:06):

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

view this post on Zulip Neil Strickland (May 29 2019 at 23:09):

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.

view this post on Zulip Chris Hughes (May 29 2019 at 23:11):

It is because of that fact.

view this post on Zulip Neil Strickland (May 29 2019 at 23:14):

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.

view this post on Zulip Floris van Doorn (May 29 2019 at 23:17):

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

view this post on Zulip Rob Lewis (May 29 2019 at 23:31):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 23:32):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 23:32):

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

view this post on Zulip Floris van Doorn (May 29 2019 at 23:36):

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

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

view this post on Zulip Floris van Doorn (May 29 2019 at 23:41):

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.

view this post on Zulip Chris Hughes (May 29 2019 at 23:46):

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.

view this post on Zulip Floris van Doorn (May 29 2019 at 23:48):

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.

view this post on Zulip Floris van Doorn (May 30 2019 at 01:31):

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

view this post on Zulip Neil Strickland (May 30 2019 at 06:59):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 07:40):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 07:41):

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

view this post on Zulip Kenny Lau (May 30 2019 at 07:42):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 07:48):

certainly not. I think isabelle has the only known proof

view this post on Zulip Mario Carneiro (May 30 2019 at 07:48):

oh, Freek says there are also others

view this post on Zulip Mario Carneiro (May 30 2019 at 07:49):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 07:49):

you have to build proof theory first

view this post on Zulip Kenny Lau (May 30 2019 at 07:51):

I thought someone proved it in the conference we went to

view this post on Zulip Kenny Lau (May 30 2019 at 07:52):

I remember the independence of continuum hypothesis having been proved

view this post on Zulip Kenny Lau (May 30 2019 at 07:52):

so there is definitely a proof theory

view this post on Zulip Mario Carneiro (May 30 2019 at 07:53):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 07:53):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 07:55):

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

view this post on Zulip Scott Morrison (May 30 2019 at 07:55):

@Martin Skilleter has the Cauchy-Schwarz inequality.

view this post on Zulip Patrick Massot (May 30 2019 at 08:42):

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.

view this post on Zulip Mario Carneiro (May 30 2019 at 08:47):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 08:48):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 08:48):

it's really a statement about a whole construction

view this post on Zulip Keeley Hoek (May 30 2019 at 08:48):

Perhaps a link to the "main" file?

view this post on Zulip David Michael Roberts (May 30 2019 at 10:27):

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?)

view this post on Zulip Mario Carneiro (May 30 2019 at 10:32):

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)

view this post on Zulip David Michael Roberts (May 30 2019 at 11:56):

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

view this post on Zulip David Michael Roberts (May 30 2019 at 11:58):

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

view this post on Zulip Floris van Doorn (May 30 2019 at 16:33):

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

view this post on Zulip Floris van Doorn (May 30 2019 at 16:36):

@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.

view this post on Zulip Mario Carneiro (May 30 2019 at 16:37):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 16:38):

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

view this post on Zulip Floris van Doorn (May 30 2019 at 16:39):

@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.

view this post on Zulip Floris van Doorn (May 30 2019 at 16:42):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 16:43):

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

view this post on Zulip Reid Barton (Jun 01 2019 at 06:43):

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.

view this post on Zulip Reid Barton (Jun 01 2019 at 07:07):

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

view this post on Zulip Alex J. Best (Jun 11 2019 at 09:19):

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

view this post on Zulip Johan Commelin (Jun 11 2019 at 09:26):

Wow, that's almost 500 lines of proof!

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 09:58):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 09:59):

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

view this post on Zulip Alex J. Best (Jun 11 2019 at 09:59):

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.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 10:00):

wait, I spoke too soon :-/

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 10:01):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 10:01):

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.

view this post on Zulip Alex J. Best (Jun 11 2019 at 10:07):

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!

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 10:09):

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.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 10:12):

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.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 10:14):

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

view this post on Zulip Alex J. Best (Jun 11 2019 at 10:25):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 11:14):

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.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 11:14):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 11:16):

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.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 11:18):

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

view this post on Zulip Alex J. Best (Jun 11 2019 at 12:10):

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.

view this post on Zulip Alex J. Best (Jun 11 2019 at 22:40):

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?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 22:48):

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

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 22:50):

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

view this post on Zulip Floris van Doorn (Jul 01 2019 at 11:38):

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

view this post on Zulip Floris van Doorn (Jul 01 2019 at 12:59):

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?

view this post on Zulip Johan Commelin (Jul 01 2019 at 20:48):

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

view this post on Zulip Floris van Doorn (Aug 06 2019 at 21:40):

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.

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 22:02):

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

view this post on Zulip Floris van Doorn (Aug 06 2019 at 23:06):

thanks, I fixed the title.

view this post on Zulip Johan Commelin (Sep 01 2020 at 08:14):

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

view this post on Zulip Rob Lewis (Sep 01 2020 at 08:16):

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

view this post on Zulip Floris van Doorn (Jan 08 2021 at 19:57):

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

view this post on Zulip Kevin Buzzard (Jan 08 2021 at 20:35):

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

view this post on Zulip Floris van Doorn (Jan 08 2021 at 23:33):

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

view this post on Zulip Ruben Van de Velde (Jan 09 2021 at 09:01):

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

view this post on Zulip Kenny Lau (Jan 09 2021 at 09:02):

I don't think it should be hard.

view this post on Zulip Johan Commelin (Jan 09 2021 at 09:07):

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

view this post on Zulip Kevin Buzzard (Jan 09 2021 at 09:46):

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

view this post on Zulip Chris Hughes (Jan 09 2021 at 11:44):

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

view this post on Zulip Ruben Van de Velde (Jan 09 2021 at 11:46):

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

view this post on Zulip Johan Commelin (Jan 09 2021 at 13:48):

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


Last updated: May 15 2021 at 22:14 UTC