Remaining 100 theorems

Stream: mathlib4

[Johan Commelin]

https://leanprover-community.github.io/100-missing.html shows that there are 20 items on the list missing.

Let's use this thread to record WIP. Just to get an overview.

• 5: Prime Number Theorem

  • WIP: see #PrimeNumberTheorem+

• 8: The Impossibility of Trisecting the Angle and Doubling the Cube

  • WIP: Links: Github, dependency graph

• 12: The Independence of the Parallel Postulate

• 13: Polyhedron Formula

• 21: Green’s Theorem

• 28: Pascal’s Hexagon Theorem

• 29: Feuerbach’s Theorem

• 32: The Four Color Problem

• 33: Fermat’s Last Theorem

  • WIP: see #FLT (but the goal atm is not a 100% verification)

• 41: Puiseux’s Theorem

• 43: The Isoperimetric Theorem

• 47: The Central Limit Theorem

  • WIP: see https://remydegenne.github.io/CLT/index.html

• 48: Dirichlet’s Theorem

  • WIP: see #PR reviews > Prerequisites for PNT and Dirichlet's Thm

• 50: The Number of Platonic Solids

• 53: Pi is Transcendental

  • WIP, see 56 below

• 56: The Hermite-Lindemann Transcendence Theorem

  • WIP, see PR #6718

• 61: Theorem of Ceva

  • Lean 3 wip: !3#10632

• 84: Morley’s Theorem

• 87: Desargues’s Theorem

• 92: Pick’s Theorem

[Johan Commelin]

@Michael Stoll you have 48: Dirichlet’s Theorem on your radar, right? [found a relevant thread]

[Markus Himmel]

92: Pick's Theorem appears in Proofs from the Book, so https://github.com/mo271/FormalBook https://firsching.ch/FormalBook/blueprint/sect0013.html#pick_theorem could be considered WIP towards it.

[Johan Commelin]

Aah, nice. But nobody is really working on the formalization atm, right? Maybe @Dhyan Aranha and #Proofs from the book are interested?

[Rémy Degenne]

The CLT project is not being actively worked on right now, but some of the prerequisites described in the blueprint are in progress (by other people who may have other end goals). See PR #18775 for example.

[Michael Rothgang]

I saw a PR about 61 (Ceva) a while back (6-12 months?), which was never merged. I can't find the PR on mathlib or mathlib4, though. @Joseph Myers

[Ruben Van de Velde]

It's been a long time since I saw Green's theorem, but it feels like something that could be a special case of some absurdly general result about integrals that we already have. Maybe @Sébastien Gouëzel has thoughts?

[Sébastien Gouëzel]

For me, Green's theorem is a particular case of Stokes theorem, which we don't have yet because we don't have differential forms.

[Yaël Dillies]

Michael Rothgang said:

I saw a PR about 61 (Ceva) a while back (6-12 months?), which was never merged. I can't find the PR on mathlib or mathlib4, though. Joseph Myers

It was @Mantas Baksys and I. It's certainly close to completion. I could give it another stab

[Johan Commelin]

Do you have the PR number?

[Yaël Dillies]

!3#10632

[Floris van Doorn]

I had a student @Ludwig Monnerjahn working on 8, and he is mostly done. Unfortunately, his Bachelor project ended before he finished the full formalization, and I'm not sure if he has time to finish it (he did mention that he wanted to finish it). Links: Github, dependency graph

[Floris van Doorn]

It's funny how many of the remaining theorems are elementary planar Euclidean geometry.

[Johan Commelin]

I think it highlights that this list is quite disconnected from modern maths.

[Jireh Loreaux]

It also highlights how much we're lagging in elementary planar Euclidean geometry. :laughing:

[Jireh Loreaux]

I realized for the first time just now that 92: Pick's theorem is not referring to the Schwarz-Pick theorem. Arguably they're both geometry!

[Johan Commelin]

Maybe we should formalize that one instead :rofl:

[Joseph Myers]

I don't think Ceva is close to completion, that PR is all specific to the case of triangles in a two-dimensional space (using affine bases), when nothing should require the simplex to be top-dimensional and most things shouldn't be specific to triangles either (triangles should just be a special case deduced at the end).

[Joseph Myers]

13 and 32 involve planar graphs. People have talked about doing combinatorial maps (in variable levels of generality - do you want to cover n-dimensional maps, surfaces other than the plane, etc.?) from time to time but we haven't yet seen things reach mathlib.

[Joseph Myers]

28 and 87 are projective geometry, so should be done first for projective spaces over arbitrary fields (don't know if any complications arise for conics in characteristic 2) with Euclidean versions only then following as a special case. Various people have expressed an interest in projective geometry, but it doesn't seem to have got as far as getting these results into mathlib.

[Joseph Myers]

As for 12, various people have done things with axiomatic geometry - but not as far as axiomatizing geometry without the parallel postulate and classifying all the models of those axioms, or at least not getting that into mathlib.

[Joseph Myers]

For Pick's theorem, we still need to establish a good way of talking about m-dimensional volume (in an n-dimensional Euclidean affine space where maybe n > m) for all geometrical results concerning area and volume (cf. the discussions of Hausdorff measure normalization), though that didn't stop people putting ad hoc versions of area of a circle and Heron's formula in the mathlib archive without such a standard and general notion of volume. (And we also need appropriate notions of a polygon and its interior.)

[Ruben Van de Velde]

rss-bot said:

feat(Wiedijk100Theorems): roots of a quartic (mathlib4#18290)

• Added quartic_eq_zero_iff which gives the roots of the quartic equation in terms of a root u to a particular cubic equation, and a degenerate case quartic_eq_zero_iff_of_q_eq_zero
• Simplified the cubic proof

Authored-by: hanwenzhu (commit)

This brings us up to 80; maybe a good point to ask Freek to update his page (it still has Lean at 76)

[Riccardo Brasca]

We should also update https://leanprover-community.github.io/100.html

[Ruben Van de Velde]

That should happen as soon as the documentation cron job runs, I think

[Rida Hamadani]

There are many versions of the isoperimetric inequality, does proving any one of them suffice to cross it off the list?

[Yaël Dillies]

See #maths > Isoperimetric Inequality

[Kevin Buzzard]

Freek has a very liberal interpretation of what counts. For example IIRC the Isabelle proof of the pythagorean theorem is something like "def d (a b : R^2) : R := sqrt((a.1-b.1)^2+(a.2-b.2)^2)"

[Johan Commelin]

The docs have been updated. I've sent Freek a ping.

[Johan Commelin]

@Joseph Myers Should Desargues even be done over noncomm division rings (aka skew fields)?

[Alex Kontorovich]

Johan Commelin said:

• 5: Prime Number Theorem
  • WIP: see #PrimeNumberTheorem+

The PNT itself was finished on Apr 8 (see https://leanprover.zulipchat.com/#narrow/channel/423402-PrimeNumberTheorem.2B/topic/Connecting.20with.20EulerProducts.2FPNT.2Elean/near/431950693); now we're working on cleaning things up, getting stronger versions of the theorem (error terms), generalizations (and getting ever closer to 48, Dirichlet...)

[Johan Commelin]

Aaah, do you already want to add this to docs/100.yaml? Or do you want to wait with that till it hits mathlib?

[Alex Kontorovich]

I suppose if the metric is "formalized in Lean" (as opposed to Mathlib), then we can probably just add it already. (It'll take quite a bit more time to clean up the proof enough to get it into Mathlib...)

[Johan Commelin]

Yeah, the metric is "formalized in Lean". Otherwise we can't have independence of CH on our list (-;

[Michael Rothgang]

So 53 and 56 (Lindemann-Weierstrass) could be added to the list already, right?

[Johan Commelin]

Yeah, but I would prefer to have some sort of stable reference that is not a PR number.

[Johan Commelin]

So a separate repo, or something in mathlib.

[Joseph Myers]

Johan Commelin said:

Joseph Myers Should Desargues even be done over noncomm division rings (aka skew fields)?

I don't know what projective geometry works in the noncommutative case and what doesn't.

[David Michael Roberts]

So Lean has overtaken Coq in the list (when it's updated)? Nice.

[Edward van de Meent]

That is of course assuming they dont have a similar backlog of updates

[Patrick Massot]

David Michael Roberts said:

So Lean has overtaken Coq in the list (when it's updated)? Nice.

Please, please, don’t start bragging about that. It’s really a non-event about an absurd list.

[Mauricio Collares]

I just noticed that @Freek Wiedijk's page starts by saying 'There used to exist a "top 100 of mathematical theorems" on the web', but the original list still exists at http://pirate.shu.edu/~kahlnath/Top100.html

[Pieter Cuijpers]

Freek gave a talk at RU a few weeks ago, discussing 1000 theorems rather than 100.
In short, he once had a side-project linking formalizations to the wikipedia list of mathematical theorems.
But of course, that list is rather daunting if taken as a short-term goal now that Lean is getting close to completing the 100.

[Ruben Van de Velde]

"Close to completing" is a bit of a stretch if you count FLT :)

[Joseph Myers]

We could probably get to 50 or 100 pretty quickly on a list of all theorems covered in Wikipedia simply by identifying all those that have in fact been done in Lean already, and quite a few more by finding all the elementary ones that are easy to prove given the current state of mathlib. (The Wikipedia "List of theorems" itself is rather more arbitrary and incomplete and not reliably updated when people write about new theorems. I suspect starting from https://en.wikipedia.org/wiki/Category:Theorems and working down the categories hierarchically and then eliminating all pages that don't cover anything that could be considered a mathematical theorem, and adjusting for pages that discuss more than one theorem, would give something more complete and less arbitrary - though still maybe less thorough about theorems covered on pages whose overall topic is some kind of mathematical object to which the theorem relates rather than the theorem itself, which are less likely to be in such categories.)

[Mario Carneiro]

I believe Freek's idea here is that if you think a theorem should be on the "List of Theorems", then you should edit the page and let wikipedia moderation do its job

[Mario Carneiro]

I feel like second guessing the methodology is only useful up to a point, because this has been under development for a few months and it has some infrastructure now. I am worried that it is open to endless bikeshedding and we'll never get another benchmark beyond the 100 theorems list if we keep it up

[Johan Commelin]

There is already another benchmark: undergrad.yaml

[Johan Commelin]

That one is very well-defined.

[Mario Carneiro]

I think it's also nearing the end of its useful life though

[Mario Carneiro]

it is good to have benchmarks that are only 20% complete and not 90+% complete

[Mario Carneiro]

Also, for it to be useful comparing across libraries I think undergrad.yaml needs to be advertised more to other theorem proving communities

[Mario Carneiro]

and the fact that it has been a benchmark for lean for a while gives lean what will be perceived as an unfair advantage on the list

[Mario Carneiro]

i.e. it has much more bias issues than a new wikipedia based list

[Floris van Doorn]

I think it would be nice to start filling in what has been already formalized of the 1000-theorems list. For this, it would be good to first set up a bit of infrastructure so that we can start more easily filling out the entries (and keep the data in Mathlib so that we will notice if something gets renamed). I posted my thoughts on this here.

[Yaël Dillies]

Can't wait for the 10000 theorems list :sweat_smile:

[Joseph Myers]

Where is the infrastructure used for updating the 1000-theorems list from Wikipedia when the list there changes (or indeed that used to create the original list from Wikipedia, if the support for in-place updates hasn't yet been written)? I couldn't locate any infrastructure related to updates from Wikipedia in https://github.com/1000-plus/1000-plus.github.io (which also looks rather inactive at present).

I raised the question of the scope of the Wikipedia list of theorems last month on its talk page (with a view to seeing if it would be appropriate to add entries more systematically for theorems only omitted because they are called "lemma", "identity", "inequality", "formula", "classification", "law", "conjecture" etc. rather than "theorem", or because they appear as part of a Wikipedia page on a larger topic rather than their own page). One response suggested that actually the page should be deleted under current Wikipedia practice, and they may have a good point (it's a very old page, added around the time Wikipedia first gained categories at all as an alternative to lists, and not well maintained lately). (A couple of other people have added theorems to the list, probably in response to the discussion drawing attention to it.)

What I don't have a sense of is how incomplete the Wikipedia list is: whether adding all theorem pages not currently in the list (but found via Category:Theorems or having various key words in the page title) would result in a list 10% longer, or twice as long or more.

[Floris van Doorn]

I think @Freek Wiedijk is still writing this script (or has a version that is not yet in the repository).
We know that the Wikipedia list of theorems is somewhat arbitrary, but we wanted to use an outsider source of information, and not decide ourselves what is a theorem.
if the Wikipedia page gets removed, then we should use another source, such as the pages in the Category:Mathematical_theorems (including subcategories).

[Riccardo Brasca]

Is anyone working on number 41, Puiseux’s Theorem? I am thinking about giving it to a student (but I have to check the math proof)

[Johan Commelin]

I'm not aware of any work on it.

[Antoine Chambert-Loir]

Riccardo Brasca said:

Is anyone working on number 41, Puiseux’s Theorem? I am thinking about giving it to a student (but I have to check the math proof)

If you want it for power series, you'd better have mathlib being able of computing with them (Maria-Ines and I have a bunch of PR in this direction which are stuck by a redefinition of ring topologies…).

You can have it for convergent series too, and then you need the inverse function theorem in the analytic category.

Whatever point if view, some arguments require basics of Newton polygons. (There is an elementary and detailed proof in my Field guide to algebra/Algèbre corporelle.)

[Riccardo Brasca]

Yeah, it seems a little too hard mathematically for my students. I have to think about another problem :sweat_smile:

[Yaël Dillies]

@Artie Khovanov has work towards Puiseux (unless I am deeply confused)

[Artie Khovanov]

Yaël Dillies said:

Artie Khovanov has work towards Puiseux (unless I am deeply confused)

I haven't done anything in this direction. I am working towards real closed fields (RCFs) in Lean, and I proved a generalisation of Puiseux's theorem to RCFs in Isabelle, but my Isabelle work was on RCFs rather than the core lifting / Hensel argument in Puiseux's theorem.

[Yaël Dillies]

/me was deeply confused

[Sébastien Gouëzel]

Antoine Chambert-Loir said:

You can have it for convergent series too, and then you need the inverse function theorem in the analytic category.

This one we have (well, maybe not written out explicitely, but we know that analytic functions are strictly differentiable, that strictly differentiable functions with an invertible derivative have a local inverse, and that if an analytic function has a local inverse then its inverse is analytic).

[Jineon Baek]

An effort for 43: The Isoperimetric Theorem is being made on: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Brunn-Minkowski.20Inequality.20.2B.20Theory

[Artie Khovanov]

Antoine Chambert-Loir said:

Riccardo Brasca said:

Is anyone working on number 41, Puiseux’s Theorem? I am thinking about giving it to a student (but I have to check the math proof)

Whatever point if view, some arguments require basics of Newton polygons. (There is an elementary and detailed proof in my Field guide to algebra/Algèbre corporelle.)

There are proofs of Puiseaux's theorem which don't require anything about Newton polygons. You do a bunch of coordinate transformations on your polynomial to turn the Puiseux series coefficients into power series, then apply Hensel's lemma to lift a factorisation over your (algebraically closed) base field to one over the power series ring.
eg see Algebraic Geometry for Scientists and Engineers by Abhyankar

[Notification Bot]

14 messages were moved from this topic to #mathlib4 > Ceva's theorem by Yaël Dillies.