Zulip Chat Archive

Oliver says we are welcome to use his list, and he gave me the latex source and gave permission to use it. (He also said he's interested in adding a paragraph about interactive theorem provers in the second half of his article.)

I've made a yaml file out of it: is there anyone interested in taking over to make a html template file?

My yaml file currently looks like:

5:
  area : Probability
  satz : $\overline{(X_1+X_2+ \cdots + X_n)} \to Z$ in distribution.
  long : |
    Given a sequence $X_k$ of **independent random variables** on a
    probability space $(\Omega,\mathcal{A},{\rm P})$ which all have the same
    **cumulative distribution functions** $F_X(t) = {\rm P}[X \leq t]$. The
    **normalized random variable** $\overline{X}=$ is
    $(X-{\rm E}[X])/\sigma[X]$, where ${\rm E}[X]$ is the **mean**
    $\int_{\Omega} X(\omega) dP(\omega)$ and
    $\sigma[X]  = {\rm E}[(X-{\rm E}[X])^2]^{1/2}$ is the standard
    deviation. A sequence of random variables $Z_n \to Z$ **converges in
    distribution** to $Z$ if $F_{Z_n}(t) \to F_Z(t)$ for all $t$ as
    $n \to \infty$. If $Z$ is a **Gaussian random variable** with zero mean
    ${\rm E}[Z]=0$ and standard deviation $\sigma[Z]=1$, the **central limit
    theorem** is:

    > $\overline{(X_1+X_2+ \cdots + X_n)} \to Z$ in distribution.

    Proven in a special case by Abraham De-Moivre for discrete random
    variables and then by Constantin Carathéodory and Paul Lévy, the theorem
    explains the importance and ubiquity of the **Gaussian density
    function** $e^{-x^2/2}/\sqrt{2\pi}$ defining the **normal
    distribution**. The Gaussian distribution was first considered by
    Abraham de Moivre from 1738. See [@Stroock; @knillprobability].

I would suggest that a good presentation would be to only show the "area" and "satz" (Knill's term for the pithy version of the statement), as well as any "author" and "decl" fields we add as links to mathlib. Possibly clicking on an item should unfold the "long" description.

I think with a list like this, where we are not very far along at the moment, it is better to display the entire list, with clear formatting showing which ones are in mathlib and which ones aren't (green and red shaded backgrounds?)

Scott Morrison (Aug 06 2020 at 07:16):

If anyone would like to play with this it is on the knill branch of the leanprover-community.github.io repository.

Scott Morrison (Aug 06 2020 at 07:39):

(This is probably only worth working on if we actually think it would be good to redirect some attention from Freek's 100 list to this list. But that may in fact be the case.)

Kevin Buzzard (Aug 06 2020 at 07:59):

The big problem with Freek's list is that the vast majority have been done (and FLT is a joke) so it gives a very misleading impression

Kevin Buzzard (Aug 06 2020 at 07:59):

This would give a far more meaningful impression of what needs to be done

Kevin Buzzard (Aug 06 2020 at 08:00):

To be honest I think that the first challenge is to state 90% of them

Jacques Carette (Aug 06 2020 at 20:47):

I'm sure you meant this implicitly, but let's make it explicit: stating 90% of them on top of the same unified library of concepts.

Mizar has gotten really far, but at the cost of duplicating a lot of definitions [the Mizar authors themselves have complained about this in print.]

Reid Barton (Aug 07 2020 at 00:26):

Why did they end up duplicating definitions?

Reid Barton (Aug 07 2020 at 00:26):

Independent developments that covered the same ground?

Yury G. Kudryashov (Aug 07 2020 at 05:43):

AFAIK, they publish new "papers" instead of updating old ones.

Yury G. Kudryashov (Aug 07 2020 at 05:44):

(I don't remember how they call mini-libraries)

Yury G. Kudryashov (Aug 07 2020 at 05:45):

This way you know for sure that your dependencies won't change but if you want to refactor a definition, then you have to "republish" all reverse dependencies.

Yury G. Kudryashov (Aug 07 2020 at 05:47):

Disclaimer: I may be wrong. I think I've spent less than a day looking at Mizar. I disliked the idea of an interpreted with source available only to people who actively used the binary for some time.

Jacques Carette (Aug 19 2020 at 14:32):

@Reid Barton (sorry for the slow answer, this got buried). In part, it is because of what @Yury G. Kudryashov mentions. But also, there is definitely the issue that there was no curation of the library, no 'gatekeeper' that suggested that things should build on one another. What happens is that different (but equivalent) definitions provide different levels of convenience in different contexts.

But also, there is a definite first-mover effect: Mizar was first at so many things, slowing people down by requiring that they must build a coherent whole we it's unclear that the parts themselves are even possible, is/was simply too high a bar. Only in retrospect can we see that this led into chaos.

Note that Coq has the same problem. They are trying to fix it, but it is difficult.

The problems are well-known: none of the current theorem provers have good abstraction facilities. By 'abstraction' here I mean the CS structural version of that, as obviously most of them are happy quantifying over all sorts of stuff that are increasingly 'abstract' from a math POV. This is why we have the bundling/unbundling problems (save for Arend), that so much ink has been written about coerce and transport, that we need to care about 'definitional equality', proof (ir)relevance and so on.

In other words, my opinion is that 'mathematics' as a _unified whole_ does not yet exist. And that it will be quite a bit of hard (potentially thankless) work to do so. Because, as others have said, mathematicians do know what they are doing, so it _will_ work.

Jacques Carette (Aug 19 2020 at 14:41):

I'm (a little perversely) quite pleased to see all the struggles with finset and fin in a variety of discussions. In my opinion, this is one of the symptoms of the gap between 'semantic' mathematics and the convenient-on-paper-only short-cuts that are used all the time.

Math uses indexing a lot, but because all the theorems you need to be true for dealing with indexing really are true (lots of finite combinatorics at play), there is simply not reason to worry on-paper. But when you try to be precise, wow does it ever become a mess. Linear Algebra, multivariate polynomials and Multicategories were the two things that brought this into focus for me. (Following the 'Universal Algebra' method of looking at things, eventually you wonder why polynomials seem to inhabit this weird half-semantic, half-syntactic worlds, and so you ask What is the theory of polynomials and get some super gratifying answers).

Johan Commelin (Oct 03 2020 at 17:02):

@Scott Morrison I only found this thread now... and I think we should do something with this list (even if it isn't urgent).

Johan Commelin (Oct 03 2020 at 17:03):

What do you think of having the satz, but then also sub-items for every term printed in bold?

Johan Commelin (Oct 03 2020 at 17:03):

That would give an extremely long list, but I don't think that's a problem.

Johan Commelin (Oct 03 2020 at 20:17):

136 also seems curious:

There is no theorem about the Mandelbulb $M_{n,m}$ for $n>2$

Kyle Miller (Oct 03 2020 at 22:38):

Jacques Carette said:

(Following the 'Universal Algebra' method of looking at things, eventually you wonder why polynomials seem to inhabit this weird half-semantic, half-syntactic worlds, and so you ask What is the theory of polynomials and get some super gratifying answers).

I've been playing around with universal algebra in Lean, so I wanted to see how polynomial rings work as universal objects. Here's a gist: https://gist.github.com/kmill/546049b5251afdcea9acc7564e7c4fa5

It uses the formulation that polynomial ring construction is left adjoint to the forgetful functor from pointed commutative rings to commutative rings. (I didn't prove anything about the structure of the polynomial ring though.)

Jeremy Tan (Jul 24 2023 at 09:00):

(Came here after writing #6091, which is a new list of 100 theorems to formalise)

Jeremy Tan (Jul 24 2023 at 09:01):

Regarding mutilated chessboard, I had actually included a second part to my statement: Gomory's theorem which states that if two _opposite colour_ squares are removed the remainder can _always_ be domino tiled

Jeremy Tan (Jul 24 2023 at 09:02):

But yes, I agree that there is assez de formalisation vis-à-vis this, and have replaced it with the Robertson–Seymour theorem

Yaël Dillies (Jul 24 2023 at 09:28):

Do you know that Freek Wiedijk is currently compiling a new list himself?

Jeremy Tan (Jul 24 2023 at 09:50):

If he is doing that I haven't found any updates

Jeremy Tan (Jul 24 2023 at 09:51):

(i.e. that is unexpected news to me)

Yaël Dillies (Jul 24 2023 at 10:02):

I believe it is not yet public.

Yury G. Kudryashov (Jul 24 2023 at 14:36):

In some sense, both "misc" theorems can be labeled "Dynamical Systems". As for the shape of a drum, there are several results that are not about examples: e.g., H. Weyl's (1911) and V. Ivrii's (1980) estimates on the asymptotics of the spectrum. The latter estimate is conditional on a geometric assumption (the measure of periodic orbits in the corresponding billiard is zero) that is conjectured to be always true.

Jason Rute (Jul 24 2023 at 14:48):

This PA question might be relevant: https://proofassistants.stackexchange.com/questions/436/impact-of-formalizing-100-theorems-and-what-is-next

Moritz Doll (Jul 24 2023 at 19:50):

Yury G. Kudryashov said:

As for the shape of a drum, there are several results that are not about examples: e.g., H. Weyl's (1911) and V. Ivrii's (1980) estimates on the asymptotics of the spectrum. The latter estimate is conditional on a geometric assumption (the measure of periodic orbits in the corresponding billiard is zero) that is conjectured to be always true.

Do you know whether there is any research area that considers similar questions to that conjecture? I know a bit about the PDE part of the story (by the way manifolds without boundary are way better than domains and there are lots of interesting theorems there), but I have no clue about the dynamical systems side.

Yury G. Kudryashov (Jul 24 2023 at 20:31):

Yeah, half of my PhD thesis says that in a planar domain with a sufficiently smooth boundary, the measure of quadrilateral periodic trajectories is zero. For triangular trajectories, this is known in any dimension (Rychlik, Vorobets, ...)

Yury G. Kudryashov (Jul 24 2023 at 20:36):

This is also related to the following question: is it possible to hide an object with mirrors? More precisely, we want a system of mirrors (hypersurfaces) such that all rays going from the camera (a) never visit some domain; (b) after some reflections, go to infinity along the same rays. For a camera fixed at a point, the answer is "yes", but what if one can put the camera anywhere in a small nhd of a given point? The question differs from Ivrii's by signs at 2 intersections, so, e.g., from the complex point of view, it is the same question.

Joseph Myers (Jul 24 2023 at 23:19):

It's good that the list in #6091 includes statements or references for the theorems, considering that the old 100 theorems list suffered from having just names, some of which were rather obscure as to what result was intended, especially in the cases where it's not clear where the dividing line between theorem and definition is (triangle inequality, Pythagoras, ...) - I hope any new list Freek compiles also includes statements and references like that. Though whatever the right location for such lists is, a single GitHub issue doesn't seem ideal for what's clearly 100 separate projects (many of which could have many sub-issues - or a whole blueprint - or a giant project taking many years of work).

Mario Carneiro (Jul 24 2023 at 23:23):

the lack of explicit statements was IIRC deliberate, stating the theorem is part of the challenge and it can be problematic if the statement is formulated by someone who doesn't have the domain knowledge to do it right (often times no such person even exists at the time the challenge is originally posed!)

Mario Carneiro (Jul 24 2023 at 23:24):

I don't recall ever having difficulty locating the theorem by name, they all have wikipedia pages

Yury G. Kudryashov (Jul 24 2023 at 23:28):

E.g., difficulty of formalizing triangle inequality or Pythagoras highly depends on how do you formulate them.

Yury G. Kudryashov (Jul 24 2023 at 23:29):

In the 1st case: which metric space; in the second case: is it about a Hilbert space or an axiomatically defined plane?

Joseph Myers (Jul 24 2023 at 23:30):

The statements in #6091 aren't (and don't need to be) fully detailed statements at the level of e.g. the official Millennium Prize Problem descriptions that define exactly what does or does not qualify as a solution; they're still better than just giving abbreviated names. Names such as "The Partition Theorem" are, by themselves, rather obscure (there are lots of theorems about partitions!).

Mario Carneiro (Jul 24 2023 at 23:32):

Yury G. Kudryashov said:

In the 1st case: which metric space; in the second case: is it about a Hilbert space or an axiomatically defined plane?

It's up to you, that's the point. What are you going to formalize? It says something about the library how it approaches this question

Mario Carneiro (Jul 24 2023 at 23:33):

I think this bit of underspecification is actually a good trick, it is like a Rorschach test for the library when you look at how all the statements differ across libraries

Scott Morrison (Jul 24 2023 at 23:35):

It also helps encourage not taking languages' scores against the list too seriously. :-)

Mario Carneiro (Jul 24 2023 at 23:36):

I understand and agree with the point re: theorem names which are so vague that it is unclear what they are referring to (Euler's theorem anyone?), although I think "The Partition Theorem" isn't one of them, AFAICT there is only one theorem that claims to be "the partition theorem"

Mario Carneiro (Jul 24 2023 at 23:37):

a link to a wikipedia page is usually enough to clear that up

Joseph Myers (Jul 24 2023 at 23:47):

I think having a new list of formalization targets is worthwhile, but ideally it would look somewhat different to the old list, reflecting the different challenges for formalization today. The challenge now isn't so much "can we formalize X?" for various X - by now it's clear that just about any individual result X can be formalized on its own with enough effort. And the old list effectively provided lots of examples of such individual results.

Rather, I think challenges now are more about issues such as scaling, breadth, integration, maintenance. Can mathlib scale to 100 times its present size, with a community 100 times its present size and commits going in at 100 times the present rate? Can it reach the point where it has not merely most of an undergraduate degree but many of the key results used by people working in all fields of mathematics? Can all the results be formalized not just on their own, but with all the underlying mathematics being properly integrated in mathlib? Will the proofs be maintained afterwards (arguably several of the entries on Freek's original list should now have some kind of red flag in the list of Lean proofs, that they were only done in Lean 3 in an external repository and so haven't been done in Lean 4 / with current mathlib4 - and I'd guess much the same applies for some of the other theorem provers that have been used to formalize entries on that list)?

Considering those challenges suggests that maybe some of the following would make sense for a new list of formalization targets. (a) It should have a lot more than 100 theorems, to provide broad coverage of different areas of mathematics. (b) It should routinely get more theorems added (whenever new results come to prominence), rather than being a fixed and frozen list (but once an entry is there, it should remain there). (c) While "interesting oddities" as described in a comment on #6091 are worth including, maybe also get people working in (or familiar with) many different fields of mathematics to suggest lists of major theorems in their fields for inclusion. (You might get the "interesting oddities" by counting "mathematics that attracts popular interest or coverage" as being a field there.) (d) There should be an associated convention that a theorem on the list isn't considered done until all the underlying mathematics is fully integrated in the relevant libraries for the theorem prover being used, with the result itself being somewhere that gets maintained on an ongoing basis independent of the original authors.

Mario Carneiro (Jul 25 2023 at 00:01):

Will the proofs be maintained afterwards (arguably several of the entries on Freek's original list should now have some kind of red flag in the list of Lean proofs, that they were only done in Lean 3 in an external repository and so haven't been done in Lean 4 / with current mathlib4 - and I'd guess much the same applies for some of the other theorem provers that have been used to formalize entries on that list)?

FWIW I consider this a strong negative aspect of lean in general: it is not suitable for doing anything "archival quality" because in a year you will have difficulty getting it to compile. Mathematics is supposed to "stay proved", and lean overhauling itself on a regular basis does not help in this regard. Not all theorem provers have this issue, although the approaches used to deal with it vary.

Mario Carneiro (Jul 25 2023 at 00:03):

Ping @Freek Wiedijk since he was specifically interested in this topic and as mentioned up-thread is working on this

Johan Commelin (Jul 25 2023 at 07:29):

Quoting from https://leanprover-community.github.io/100.html

Currently 76 of them are formalized in Lean. We also have a page with the theorems from the list not yet in mathlib.

I think we should update this sentence. Because it suggests that those 76 are in mathlib.

Johan Commelin (Jul 25 2023 at 07:30):

I agree with @Mario Carneiro that maths is supposed to "stay proved". But it is also supposed to "stay applicable". And I think there aren't many systems out there that support both features at the same time.

Mario Carneiro (Jul 25 2023 at 07:37):

the easiest way to support both features at the same time is to be a dead language :)

Johan Commelin (Jul 25 2023 at 07:38):

I'm not convinced that is sufficient.

Johan Commelin (Jul 25 2023 at 07:38):

You also need a dead library

Johan Commelin (Jul 25 2023 at 07:39):

Refactors should be forbidden.

Johan Commelin (Jul 25 2023 at 07:39):

And everything should work together smoothly from day 0.

Ruben Van de Velde (Jul 25 2023 at 07:39):

And dedicated hardware / OS?

Mario Carneiro (Jul 25 2023 at 07:39):

there is no need for that

Mario Carneiro (Jul 25 2023 at 07:40):

in fact it would be detrimental because once support for that hardware goes away there goes the archive

Eric Wieser (Jul 25 2023 at 08:03):

Regarding the website, note that until we get https://github.com/leanprover-community/leanprover-community.github.io/pull/338 past CI (discussed here) it will continue to link to mathlib3

Joseph Myers (Jul 25 2023 at 09:54):

Johan Commelin said:

Quoting from https://leanprover-community.github.io/100.html

Currently 76 of them are formalized in Lean. We also have a page with the theorems from the list not yet in mathlib.

I think we should update this sentence. Because it suggests that those 76 are in mathlib.

Of the entries on that list neither in mathlib nor the mathlib archive (but instead linking to some external project), I'd guess that Ramsey’s Theorem, Sylow’s Theorem (any bits that aren't already in mathlib), Principle of Inclusion/Exclusion aren't too hard to get into mathlib-suitable form (so eliminating the need to link to external projects for them) - whether that form is based on the implementations linked from the list, or is reproved from scratch. Probably harder to get into mathlib (but still desirable before they can really be considered to be done and to stay proved) are The Independence of the Continuum Hypothesis, Brouwer Fixed Point Theorem, e is Transcendental.

Joseph Myers (Jul 25 2023 at 09:58):

If mathlib is to scale to 100 times the present size (and the mathlib archive to 100 times the size of mathlib, potentially - if mathlib is "anything standard / in a textbook", the mathlib archive could be "formal versions of anything from the rest of the mathematics literature", though maybe the mathlib archive would no longer be a monorepo at that point), I expect we'll want really good refactoring tools to help update things when we change low-level parts of mathlib. Such tools might end up being key to how things "stay proved", if they can be applied to external projects, to branches for open PRs, etc., just as easily as they are applied to mathlib itself and the mathlib archive.

Ruben Van de Velde (Jul 25 2023 at 10:01):

There's a mathlib3 PR for e transcendental, but I stopped working on it because I thought Lindemann-Weierstrass was very close (https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lindemann-Weierstrass.20theorem.20almost.20done), but I don't think anyone is working on the missing part

Joseph Myers (Jul 25 2023 at 10:05):

If someone does complete that - and get it into mathlib4! - then that's certainly one way of eliminating a dependence on an old external project for an entry on the 100 theorems list (and, at the same time, moving 53: Pi is Transcendental and 56: The Hermite-Lindemann Transcendence Theorem to the list of those done in Lean).

Johan Commelin (Jul 25 2023 at 10:27):

I thought there was even a sorry-free proof of L-W somewhere

Kevin Buzzard (Jul 25 2023 at 14:53):

@Jujian Zhang did transcendence of $e$ for his first Lean 3 project; it's his MSc thesis.

Ruben Van de Velde (Jul 25 2023 at 14:58):

Right, this is the PR I was referring to

Yaël Dillies (Jul 25 2023 at 16:25):

Let me mention that @Bhavik Mehta has a nice Ramsey theorem that's close to ready for inclusion in mathlib.

Alex Kontorovich (Jul 25 2023 at 17:20):

As an "analytic" number theorist, may I humbly suggest the inclusion of the Bombieri-Vinogradov theorem (the generalized Riemann hypothesis on average, for which Bombieri got his Fields Medal). Along the way, we would need to develop the large sieve, and the Siegel-Walfisz theorem, in particular dealing with issues of "ineffective" constants that cause a lot of difficulty in the subject. Would be nice to see such things formalized. But to do this the "right" way, we would first need some more complex analysis...

Joseph Myers (Jul 25 2023 at 21:19):

The proofassistants.stackexchange.com discussion linked above included a suggestion of "Fields-medal winning theorems" in general, which seems a good idea for inclusion in such a list (at least one major result for each past Fields Medal) and may help balance the interesting oddities with results considered of major importance in mathematics.

Alex Kontorovich (Jul 25 2023 at 22:02):

And of course that'll get us a lot of the way towards Zhang / Maynard, so maybe we'll get two Fields medals for the price of one...

Johan Commelin (Aug 05 2023 at 05:49):

There is a branch knill, see https://github.com/leanprover-community/leanprover-community.github.io/compare/knill?expand=1 that contains a yaml file with all the data of Knill's list of 172 theorems (thanks to Scott for wrangling the data!).
I started cargo-culting towards an html template for the corresponding web page. But I have no idea what I'm doing.

What we need to do:

Decide whether we want to add this list to our web page. (I'm strongly in favour)
Move the yaml file to the mathlib repo (just like we did with 100.yaml and undergrad.yaml)
Fix all the web templating stuff, so that it actually works
Start ticking of items in the yaml file that are already done.

Eric Wieser (Aug 05 2023 at 13:21):

We still need fix the undergrad yml to work with mathlib4

Johan Commelin (Aug 05 2023 at 13:22):

But that is orthogonal to my todo list, right?

Eric Wieser (Aug 05 2023 at 13:22):

The penultimate Todo item is the same thing

Eric Wieser (Aug 05 2023 at 13:24):

Were missing the "tell the website what filename, line number, and statement of the decl" step, which comes from the "export db" script which needs some simple meta porting

Johan Commelin (Aug 05 2023 at 13:24):

/poll Shall we turn the Knill 172 theorem list into a web page on the community website and keep track which entries are formalized in Lean?

Alex J. Best (Aug 05 2023 at 13:54):

What is the motivation for adding this list to the website? As far as I can see its a nicely written but fundamentally slightly random list of theorems (as is any list of only 100 theorems from all of mathematics). Making a webpage seems to explicitly make these theorems targets we are working towards, and we should consider carefully if these are good targets for mathlib. Personally I'd rather contributors used the projects board on github to identify useful results andpaths towards them in different sub-areas they work on, ideally results that would have a big impact on formalization in that area (e.g. unlocking deeper results, or commonly used workhorse theorems)

edit. it looks like the list actually has 272 theorems now, more than the 172 the wesite says, this is an improvement imo on the 100 version I found by googling, but still presumably less focussed than us setting our own goals

Johan Commelin (Aug 05 2023 at 14:47):

That's a fair question. I think there points that are somewhat in tension with each other:

mathlib experts know best what mathlib needs, so they should set their own goals "ideally results that would have a big impact on formalization in that area (e.g. unlocking deeper results, or commonly used workhorse theorems)"
"benchmarks" that our set outside of the community, might be somewhat "random" and hence challenge mathlib to grow in directions that might not happen naturally given the current shape of our community. They might also challenge mathlib to do things that are typically avoided because it's not a smooth or idiomatic experience. (E.g., mathlib is famously bad at explicit computational exercises.)

Johan Commelin (Aug 05 2023 at 14:47):

So, I think we should have both.

Johan Commelin (Aug 05 2023 at 14:49):

Another benefit of benchmarks, is that they can be challenges for other communities as well. My hope is that they can serve as connecting points between various communities. I think this was one of the things that happened with Freek's list, although it might be hard to quantify to what extent it happened.

Alex J. Best (Aug 05 2023 at 14:51):

Johan Commelin said:

Another benefit of benchmarks, is that they can be challenges for other communities as well. My hope is that they can serve as connecting points between various communities. I think this was one of the things that happened with Freek's list, although it might be hard to quantify to what extent it happened.

I agree with this for sure, which is partially why I'm not sure about committing to this particular list right now by putting it very visibly on the website.

Scott Morrison (Aug 05 2023 at 23:35):

Knill's list is really very good, at least in terms of reflecting "taste" of academic mathematicians. :-)

Joseph Myers (Aug 06 2023 at 23:32):

One scaling question would be how we scale to maintaining 100 overlapping lists of theorems and their status in mathlib. But while 100 separate lists may make sense as a successor to the undergraduate mathematics list (systematically list definitions and results from 100 graduate-level textbooks in different areas of mathematics, for example), it's less clear that lots of separate lists are the best form of benchmark as successors to the 100 theorems list. There, it might be better to work collaboratively with other communities to produce a 1000 theorems list as a successor to the 100 theorems list (where lists such as Knill's 272 theorems (minus any included in the 100 theorems list, or that aren't meaningful mathematical theorems that could be formalized), and those in #6091, and the supplemental theorems listed at the bottom of Freek's page, would provide ideas as a starting point for the list, but without requiring all the entries from any one such list to appear in the final 1000 theorems).

Johan Commelin (Aug 07 2023 at 04:06):

Another source of inspiration for megalists was (I think) suggested by @Joseph Corneli quite a while ago: https://en.wikipedia.org/wiki/Wikipedia:Vital_articles/Level/5/Mathematics

Joseph Myers (Aug 07 2023 at 23:58):

I think this discussion is demonstrating quite well just how many different kinds of lists of theorems there are. (Note that Knill's list is quite careful to say the "fundamental" is different from "important" or "deep"; see also Tao's What is good mathematics?. I don't think a specific list of lots of important or deep theorems has been suggested here, beyond the idea of "Fields-medal winning theorems" - and there are many more important or deep theorems that might be good candidates for formalization benchmarks than just those that won Fields Medals.)

Joseph Myers (Aug 08 2023 at 00:03):

That there are so many different ideas for the kinds of results worth including in a list of theorems for formalizing in turn I think tends to support the idea that a formalization benchmark should best be built up from suggestions from lots of people, reflecting their various preferences, in order to get a very broad range of different kinds of theorems, rather than blessing a list that reflects a single person's taste for what makes a good theorem for the list.

Yaël Dillies (Aug 16 2023 at 10:00):

Btw there's a typo in n°37 of Knill's list: The "Erdös conjecture on arithmetic progressions" should read $∑_n x_n^{-1} = ∞$ , not $∑_n x_n = ∞$ .

Damiano Testa (Aug 16 2023 at 10:25):

... or maybe it is just very easy to disprove.

Damiano Testa (Aug 16 2023 at 12:32):

Yaël's observation made me wonder how would I formalize the existence of sets containing no arithmetic progressions:

import Mathlib.Algebra.GroupPower.Order

/--  The sequence `f` does not take three values in arithmetic progression:
if there are `a b c t : ℕ` such that `f a + t = f b` and `f b + t = f c`, then
`t = 0`. -/
def No3AP (f : ℕ → ℕ) : Prop :=
∀ a b c t, f a + t = f b → f b + t = f c → t = 0

/--  The sequence `f` `grows` if the sum of two of its earlier values is smaller than
its later values. -/
def Function.grows (f : ℕ → ℕ) : Prop :=
∀ a b c, a < c → b < c → f a + f b < f c

/--  A sequence that `grows` is strictly monotone. -/
theorem Function.grows.StrictMono {f : ℕ → ℕ} (h : f.grows) : StrictMono f :=
fun x y xy ↦ lt_of_le_of_lt (by simp) (h x x _ xy xy)

/--  A sequence that `grows` satisfies `No3AP`. -/
theorem grows.No3AP (f : ℕ → ℕ) (h : f.grows) : No3AP f := by
  intros a b c t ha hb
  cases t with
    | zero => rfl
    | succ n =>
      exfalso
      have : f b + f b < f c := by
        apply h <;> refine h.StrictMono.lt_iff_lt.mp (lt_iff_exists_add.mpr ?_) <;>
        · exact ⟨n + 1, by simp [hb]⟩
      refine lt_irrefl _ (lt_of_le_of_lt ?_ this)
      rw [← hb]
      apply add_le_add_left
      rw [← ha]
      simp

/--  For `n : ℕ` with `3 ≤ n`, the sequence `{ n ^ a | a : ℕ }` does not contain
3-term arithmetic progressions. -/
-- You could tweak some inequality in `grows` and get it to work for `n = 2` as well.
theorem No3AP_pow {n : ℕ} (h2 : 2 < n) : No3AP (n ^ ·) := by
  apply grows.No3AP
  intros a b c ac bc
  wlog h : a ≤ b
  · rw [add_comm]
    refine this ?_ ?_ ?_ ?_ ?_ ?_ (Nat.le_of_not_le (by exact h)) <;> try assumption;
  apply (add_le_add (pow_mono (Nat.one_le_of_lt h2) h) rfl.le).trans_lt ?_
  show n ^ b + n ^ b < n ^ c
  rw [← two_mul]
  cases c with
    | zero => simp at ac
    | succ c =>
      rw [pow_succ]
      apply mul_lt_mul h2 ?_ ?_ n.zero_le
      · exact pow_mono (Nat.one_le_of_lt h2) (Nat.lt_succ.mp bc)
      · exact pow_pos (Nat.zero_lt_of_lt h2) ..

To disprove Erdős's conjecture, all that is left to show is that the sum of the powers of 3 diverges... :upside_down:

Yaël Dillies (Aug 16 2023 at 13:01):

No3AP is (when f is injective) docs#AddSalemSpencer

Damiano Testa (Aug 16 2023 at 13:04):

Ah, maybe I'll PR a Counterexample using AddSalemSpencer!

Damiano Testa (Aug 16 2023 at 13:05):

But sadly, I should restrain from Lean for the rest of today...

Maarten Derickx (Aug 18 2023 at 09:45):

(deleted)

Last updated: Dec 20 2023 at 11:08 UTC