doc(docs/100.yaml): add recently-proven theorems

[plby]

Two theorems from Freek Wiedijk's list of 100 theorems are currently in a Mathlib PR in progress. Five theorems from the list have been auto-formalized by Aristotle from Harmonic, and their solutions are hosted elsewhere.

---

[github-actions]

PR summary fa0ba71674

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[plby]

easy

[wwylele]

These are from the PR #28013, right? Since that PR also updates the 100 theorem list, I don't think we should merge this and cause unnecessary conflict. We should wait for the proof author to update it

[mo271]

Might still be good to merge it now, because it seems like #28013 might not be merged very soon.
I think the effort of resolving the resulting merge conflict is quite small compared to potentially wasted efforts of people trying to work on this thinking it is not yet formalised.

[plby]

Yes, this is a deep link into that PR, which has been in process for literally years.

I think the "100 theorems" page should be updated sooner rather than later to let people know this theorem has been proven in Lean. Otherwise, people can (and I have!) duplicate effort trying to prove it themselves.

I would be happy to know of a better way to link to the result, however. Maybe just the PR itself?

[plby]

I guess here's an argument for not including it at all: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Remaining.20100.20theorems/near/483043532

[jsm28]

I'm not convinced this version should take precedence over various previous versions such as leanprover-community/mathlib3#10632 - it might use a newer Lean version, but it doesn't engage any more with various past discussions (in that PR and on Zulip) of how to do things in appropriate generality as far as possible (in an arbitrary affine space with no more constraints on the ring than are needed for each individual lemma, n-dimensional as far as possible, without requiring the simplex to span the whole space), and so is equally unsuitable for inclusion in mathlib.

(Some of the other Aristotle proofs linked in this PR also fail to engage with past Zulip discussions of what a mathlib-appropriate version of the result would look like, or even invent their own definitions for things mathlib already has, but Ceva is the one where there are multiple previous proofs that all have such issues and the one linked here is just the Nth such nowhere-close-to-mathlib-ready version.)

I suppose the general principle I'm suggesting here is: this list can link to and credit the mathlib version of a theorem once it's in mathlib (and most of the results linked in this PR ought to get versions in mathlib). It can also link to and credit the first complete proof in Lean that can reasonably be considered a version of the result, if that's different from the current mathlib version. But linking to the Nth version, when N is much bigger than 1 but that version isn't in mathlib or close to getting into mathlib, is rather more questionable.

(I also have the notion that the number of results on the list that are proved in mathlib or the mathlib archive is much more interesting than the total number including those with proofs somewhere external that are probably going to bitrot and don't have reusable lemmas factored out in appropriate generality in mathlib; that proving something outside mathlib is less than half way to being done with that result and the emphasis on the lists ought to show such things as half-done not as done. But that's an objection to how these lists are presented, not a concern with an individual PR that follows the existing conventions for these lists.)

[plby]

I'm fine with 100.yaml linking to an earlier proof, but can it be linked to some proof at least? In fact, I'd be super happy if it linked to the 1st proof!

Alternatively, can the text "These theorems are not yet formalized in Lean" be changed to "These theorems are not yet formalized in Lean to a standard that Mathlib would accept"?

The general principle I'm suggesting is: can we please let the world know that these N>>1 proofs already exist!?

[jsm28]

A better approach for dealing with Ceva: just add a mathlib-appropriate version rather than doing the Nth version that doesn't attempt any kind of appropriate generality. See #33409 which tries to start things off with the forward direction (on the basis that the converse can be done later in followups).

[jsm28]

Regarding other Lean versions of Ceva: that mathlib3 PR also has a link to https://gist.github.com/anders-was-here/d786450daba4c01e40bbc5f81c681feb (described as a port of the Metamath version). The previous Zulip thread on Ceva (it would have been better to post there when talking specifically about Ceva, rather than starting a new thread) - https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ceva.27s.20theorem - has a link to https://github.com/felixpernegger/LeanCourse24/blob/master/LeanCourse/Project/Ceva.lean (as well as a start on n-dimensional Ceva by Yaël, but since that one wasn't finished it doesn't really count for the purposes of 100-theorems). So with Aristotle's and mine there are at least five sorry-free formalizations of versions of Ceva in versions of Lean.

[jsm28]

For theorems that appear both on the 100-theorems and 1000-plus lists, I think 1000.yaml should be updated at the same time as 100.yaml (and where there are multiple options to choose from, they should both link to the same formal version of a given theorem unless there is a very good reason to link to different versions).

[plby]

-awaiting-author

[Ruben-VandeVelde]

Thanks for working on this. I'm less convinced that we should have unported lean 3 formalizations in the list - it's a substantially different language. I agree that if multiple independent non-mathlib implementations exist, we should aim to list them all.

Please bring up this PR on zulip if you haven't yet, in case anyone wants to point out more examples.

[plby]

Thanks for working on this. I'm less convinced that we should have unported lean 3 formalizations in the list - it's a substantially different language. I agree that if multiple independent non-mathlib implementations exist, we should aim to list them all.

I added the Lean 3 version because this comment told me that including Aristotle's version is "questionable" and suggested that the Lean 3 version should "take precedence". (My preference is primarily that at least one thing is listed.)

[jsm28]

Since this PR-from-branch became the PR-from-fork #28013, surely linking the latter (i.e. the current version of the same formalization referenced here) is better. See my previous comment that when a result appears on both lists (and, morally, some of the entries on 100-theorems are just special cases of this one), the same formalization should be linked in each case.

[jsm28]

While I'd prefer to emphasize just those formalizations in mathlib and the mathlib archive (that thus are maintained and could all be imported together), the list does in fact have several Lean 3 formalizations on it, for The Independence of the Continuum Hypothesis (I don't think anyone's made much of an attempt at porting that to Lean 4 / mathlib model theory), Ramsey’s Theorem, Brouwer Fixed Point Theorem, e is Transcendental (this one could be subsumed by / deduced from Lindemann-Weierstrass once that's in mathlib), at least.

[ocfnash]

Are the Aristotle proofs linked here the result of autoformalisation of informal human-written proofs?

[jcommelin]

Does the script that consumes these yaml files know how to deal with such field names?

[jcommelin]

I'm hearing two opinions. Here's how I understand them, summarized in ~1-liners:

Boris: These files should take a maximally inclusive approach, if items on 100(0)?.yaml have been formalized in Lean, then those should be listed. In Lean 3 or Lean 4, mathlib, a PR, or external. Just add a link.

Joseph: Except for FLT, all items of 100.yaml have been formalized before. The genuine contribution comes from formalizing a general approach, building up the library and APIs, and getting a robust and maintainable contribution into mathlib.

Can we accomodate both of these? The logic for rendering 1000.yaml has ways to distinguish mathlib formalizations vs external ones. Can we do that for 100.yaml as well?

@plby Are you interested in reworking the script that renders 100.yaml, so that it can show a bit more metadata?

[jsm28]

I'm not suggesting that this PR should depend on reworking how the data from 100.yaml is displayed (as I said above "But that's an objection to how these lists are presented, not a concern with an individual PR that follows the existing conventions for these lists.").

What we do need to figure out for this PR is what to include when there are several different independent formalizations of versions of a result in Lean (at least five in the case of Ceva).

[jcommelin]

Maybe in such cases we could have a list?