Zulip Chat Archive

Stream: general

Topic: 100.yaml

Johan Commelin (May 22 2021 at 04:46):

Dear @Freek Wiedijk, we've managed to add a formal proof of another 5 items on your list. See https://github.com/leanprover-community/mathlib/commits/master/docs/100.yaml for recent changes to our own record of which items on the list are done.
The 5 new ones seem to be:

9:
  title  : The Area of a Circle
  links  :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/9_area_of_a_circle.lean
  author : James Arthur, Benjamin Davidson, and Andrew Souther
55:
  title  : Product of Segments of Chords
  decl   : euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi
  author : Manuel Candales
57:
  title  : Heron’s Formula
  links :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/57_herons_formula.lean
  author : Matt Kempster
77:
  title  : Sum of kth powers
  decls  :
    - sum_range_pow
    - sum_range_pow'
  author : mathlib (Moritz Firsching, Fabian Kruse, Ashvni Narayanan)
93:
  title  : The Birthday Problem
  decl   : fintype.card_embedding
  links  :
    mathlib archive: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/93_birthday_problem.lean
  author : Eric Rodriguez

Yaël Dillies (May 22 2021 at 07:06):

I didn't follow closely, but don't we have "16: Insolvability of General Higher Degree Equations" with the recent advances on Abel-Ruffini?

Johan Commelin (May 22 2021 at 09:10):

I don't think the final PR has been merged yet.

Johan Commelin (May 22 2021 at 09:10):

But I guess it will be somewhere this week.

Johan Commelin (May 22 2021 at 09:15):

Ha, the PR went off my radar. I thought there was till something to be done. But it all looks good now, so I've kicked it on the queue.
(cc @Thomas Browning)

Thomas Browning (May 22 2021 at 18:03):

Update: It's been merged:

16:
  title  : Insolvability of General Higher Degree Equations
  author: Thomas Browning
  links :
    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/16_abel_ruffini.lean

Floris van Doorn (May 22 2021 at 20:37):

I emailed Freek with a ping. I was waiting for Abel-Ruffini to be merged :)

Floris van Doorn (Jun 07 2021 at 21:20):

Freek updated his page

Oliver Nash (Jun 10 2022 at 10:51):

I think now might be a good time to email Freek again, unless Floris already sent the message he mentioned here: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313690.20strong.20law.20of.20large.20numbers/near/283733773

Eric Rodriguez (Jun 13 2022 at 08:03):

Has this been done?

Eric Rodriguez (Jun 13 2022 at 08:20):

(emailing Freek, that is)

Oliver Nash (Jun 13 2022 at 08:22):

(my question mark just indicates I don't know if the email was sent)

Floris van Doorn (Jun 13 2022 at 13:39):

Yes, I emailed Freek when I wrote the linked message. I'll ping him tomorrow.

Floris van Doorn (Jun 14 2022 at 07:22):

I pinged Freek

Floris van Doorn (Jun 21 2022 at 16:39):

Freek updated his list! He added The Fair Game theorem to the list for both Coq and Lean (the Coq formalisation was mentioned by @Koundinya Vajjha in this thread)

(I pointed out to him that there is a formatting error around/below item 62 on the list)

Kevin Buzzard (Jun 21 2022 at 16:40):

So humanity is on 98/100 right now. Anyone have any plans for doing the other viable one? (Isoperimetric inequality IIRC)

Eric Rodriguez (Jun 21 2022 at 16:41):

@Yaël Dillies said something about it recently, through a combinatorial lens somehow

Yaël Dillies (Jun 21 2022 at 16:42):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Isoperimetric.20Inequality

Yaël Dillies (Jun 21 2022 at 16:42):

I am currently working my way through Convexity by Barry Simon.

Eric Rodriguez (Jun 21 2022 at 16:43):

ah, that makes more sense

Yaël Dillies (Jun 21 2022 at 16:45):

And Sébastien sent me some resources about Prékopa-Leindler,. which is like two levels higher the generality mountain than the isoperimetric inequality.

Moritz Doll (Sep 15 2022 at 06:22):

With Taylor's theorem, we now have 73 theorems, in Freek's list Lean is still at 70.

Mario Carneiro (Sep 15 2022 at 06:22):

someone has to email Freek for the list to be updated

Johan Commelin (Sep 15 2022 at 06:28):

We used to do this after the delta got >= 5. But maybe that gap is becoming too large now?

Johan Commelin (Sep 15 2022 at 06:30):

The following are basically open PRs:

40: Minkowski’s Fundamental Theorem
53: Pi is Transcendental (as corrolary of 56 below)

Johan Commelin (Sep 15 2022 at 06:31):

56: The Hermite-Lindemann Transcendence Theorem

Johan Commelin (Sep 15 2022 at 06:33):

36: Brouwer Fixed Point Theorem (done, but no PR yet)

Floris van Doorn (Sep 15 2022 at 12:14):

I emailed Freek with the 3 new entries. It might still take a while until he updates his list.

Thomas Browning (Sep 15 2022 at 13:54):

Isn't Stirling also an open PR? (90, #14875)

Moritz Firsching (Sep 16 2022 at 09:08):

Thomas Browning said:

Isn't Stirling also an open PR? (90, #14875)

Yes, it already had a couple of review rounds, ready to go from my side..., Thanks @Moritz Doll @Thomas Browning @Sebastien Gouezel for the reviewing!

Yaël Dillies (Sep 16 2022 at 09:14):

What happened to the more general version? @James Arthur

Floris van Doorn (Sep 26 2022 at 11:01):

Freek updated the list to 73/100. I emailed him about Stirling for 74 (tied with Metamath).

Eric Rodriguez (Sep 26 2022 at 11:05):

(and he's updated that now too)

Last updated: Dec 20 2023 at 11:08 UTC