100.yaml

Stream: general

[Johan Commelin]

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]

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]

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

[Johan Commelin]

But I guess it will be somewhere this week.

[Johan Commelin]

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]

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]

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

[Floris van Doorn]

Freek updated his page

[Oliver Nash]

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]

Has this been done?

[Eric Rodriguez]

(emailing Freek, that is)

[Oliver Nash]

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

[Floris van Doorn]

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

[Floris van Doorn]

I pinged Freek

[Floris van Doorn]

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]

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

[Eric Rodriguez]

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Eric Rodriguez]

ah, that makes more sense

[Yaël Dillies]

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]

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

[Mario Carneiro]

someone has to email Freek for the list to be updated

[Johan Commelin]

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

[Johan Commelin]

The following are basically open PRs:

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

[Johan Commelin]

56: The Hermite-Lindemann Transcendence Theorem

[Johan Commelin]

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

[Floris van Doorn]

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

[Thomas Browning]

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

[Moritz Firsching]

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]

What happened to the more general version? @James Arthur

[Floris van Doorn]

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

[Eric Rodriguez]

(and he's updated that now too)

[Bryan Gin-ge Chen]

I'm thinking about changing the fields used in 100.yaml per @Michael Rothgang 's suggestion here. Is anyone aware of any external consumers of this file?

The biggest change would be to remove the decl field in favor of using decls everywhere to simplify our website code, though I guess this is actually backwards-compatible.

edit: I'm now also considering changing the number field to id, which would be a breaking change.

[Michael Rothgang]

Thanks for starting this conversation! I agree that some refactoring could usefully be done, but would propose something different from https://github.com/leanprover-community/leanprover-community.github.io/pull/561. I've commented on the PR (and created https://github.com/leanprover-community/leanprover-community.github.io/pull/563 to sketch what came to my mind).

[Ruben Van de Velde]

Don't think those links are right

[Michael Rothgang]

Fixed. Is there a linkifier for webpage PRs, by the way?

[Junyan Xu]

If the repo is renamed to get rid of the dots then the linkifier would work, e.g. leanprover-community_github_io#561