freek.yaml

Stream: general

[Johan Commelin]

Given #2686 and our recent attempts at creating yaml lists that can be auto-nicified into websites. Should we start a freek.yaml somewhere?

[Johan Commelin]

I think we already had a list somewhere of what was done

[Bryan Gin-ge Chen]

I made an issue earlier today: https://github.com/leanprover-community/leanprover-community.github.io/issues/14

[Chris Hughes]

There's a 100-thms branch with the list. I don't think that's the best place for it.

[Bryan Gin-ge Chen]

Yeah, I should have copied the link to @Floris van Doorn's list from my issue: https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md

[Johan Commelin]

Aah, right, the branch. Completely forgotten about that.

[Bryan Gin-ge Chen]

We recently moved all the other files like this to the website, so I agree that we should move the info there to the website. I don't much mind whether it's in YAML form or markdown.

[Johan Commelin]

I think it should something like

 freek:
 1:
  - title: The Irrationality of the Square Root of 2
  - decl: irr_sqrt_two
  - author: mathlib
 2:
  - title: Fundamental Theorem of Algebra
  - decl: analysis.complex.exists_root
  - author: Chris Hughes

[Johan Commelin]

All the other stuff can be auto-generated, and kept up to date. If the name of a decl changes, the check-broken-link script will notify us.

[Johan Commelin]

I've almost converted the list into a yaml

[Johan Commelin]

https://gist.github.com/jcommelin/61d3cc00744aa0b445c9f182d0044885

[Johan Commelin]

It will need a little bit of extra post-processing, I guess

[Johan Commelin]

But that is better discussed once we know exactly how we want to parse it

[Patrick Massot]

I'm not convinced this is a good idea, unless someone wants to push through this list.

[Johan Commelin]

What is the downside?

[Yury G. Kudryashov]

For No. 38 you can put real.am_gm_weighted from analysis/mean_inequalities

[Yury G. Kudryashov]

No. 46 should be in quadratic_discriminant

[Jalex Stark]

"push through this list" = "prove the rest of the theorems"?

[Patrick Massot]

This list is 100% about communication, and we are not doing well on this (arguably not so interesting) target

[Patrick Massot]

I mean we can maintained this list, but displaying on the website seems like a bad idea

[Yury G. Kudryashov]

quadratic_eq_zero_iff_discrim_eq_square

[Johan Commelin]

Maintaining is important. Because the number on Freek's website is there.

[Johan Commelin]

It better go up

[Yury G. Kudryashov]

We miss many simple problems because we have no high school geometry.

[Patrick Massot]

I wouldn't display this list anywhere before we hit 75

[Johan Commelin]

Yury G. Kudryashov said:

quadratic_eq_zero_iff_discrim_eq_square

That's not about quartics, right?

[Jalex Stark]

Johan Commelin said:

It better go up

your point is that people are "grading" the Lean theorem prover by its score on this list?

[Johan Commelin]

Patrick Massot said:

I wouldn't display this list anywhere before we hit 75

That's fine. But let's keep a log. And let's tell Freek when he should bump the number on his site.

[Patrick Massot]

Only people who use proof assistants that are above 70

[Johan Commelin]

@Jalex Stark some people do. I think Freek's list get's quite a lot of hits.

[Patrick Massot]

I'm not a fan of this list, because it has not much mathematical meaning and is very poorly specified. But indeed people know about it, and I think it can be a nice project to work on it, especially since many easy things are missing

[Rob Lewis]

I don't think the list is particularly useful. But Freek's site does get a fair amount of traffic and right now it directs here: https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md
I think it doesn't hurt to make a nicer landing page than that, since people will see it anyway. I don't care in the slightest if we link to that landing page from our site.

[Johan Commelin]

I agree, I'm not a fan either.

[Patrick Massot]

Jalex, I'm sure you can contribute a couple of them

[Johan Commelin]

Why don't we turn them into Kata? Outsource the problem (-;

[Jalex Stark]

that doesn't actually outsoruce the problem :P

[Rob Lewis]

For reference, cs.ru.nl (Freek's site) is the third biggest referrer to the mathlib repo over the last two weeks (I think). Second only to GitHub and Twitter.

[Patrick Massot]

For instance it seems we don't have 10:Euler's Generalization of Fermat's Little Theorem. If this is indeed missing then you can fill it in half an hour

[Johan Commelin]

I think we actually have it

[Patrick Massot]

People are crazy

[Johan Commelin]

git grep Euler
src/field_theory/finite.lean:/-- The Fermat-Euler totient theorem. `nat.modeq.pow_totient` is an alternative statement
src/field_theory/finite.lean:/-- The Fermat-Euler totient theorem. `zmod.pow_totient` is an alternative statement
src/number_theory/quadratic_reciprocity.lean:/-- Euler's Criterion: A unit `x` of `zmod p` is a square if and only if `x ^ (p / 2) = 1`. -/
src/number_theory/quadratic_reciprocity.lean:/-- Euler's Criterion: a nonzero `a : zmod p` is a square if and only if `x ^ (p / 2) = 1`. -/

[Rob Lewis]

Rob Lewis said:

For reference, cs.ru.nl (Freek's site) is the third biggest referrer to the mathlib repo over the last two weeks (I think). Second only to GitHub and Twitter.

Actually second by unique viewers, third by total viewers.

[Reid Barton]

I see Lean also isn't listed under Cramer's Rule (97) but I see a lot of stuff about cramer--I think this one is recent?

[Jalex Stark]

I guess I care about "first impressions" of Lean, so I'll start working at it

[Johan Commelin]

Can we first decide if we want the yaml?

[Johan Commelin]

And where to put it?

[Johan Commelin]

Editing github gists is not the best UX (-;

[Rob Lewis]

I say yes, in the website repo.

[Reid Barton]

Also The Triangle Inequality (91)

[Patrick Massot]

Triangle inequality? Again what does that mean??

[Patrick Massot]

We defined metric spaces. Does that count as triangle inequality?

[Reid Barton]

Apparently in Isabelle it means the definition of class ordered_ab_group_add_abs :upside_down:

[Patrick Massot]

Ridiculous indeed

[Reid Barton]

I think I would be more comfortable with something more like Coq's

Lemma triangle :
  forall x0 y0 x1 y1 x2 y2:R,
    dist_euc x0 y0 x1 y1 <= dist_euc x0 y0 x2 y2 + dist_euc x2 y2 x1 y1.

[Yury G. Kudryashov]

Then we have this for real_inner_product spaces

[Yury G. Kudryashov]

(through an instance)

[Patrick Massot]

Should we also claim Pythagoras then?

[Yury G. Kudryashov]

The Mean Value Theorem: exists_deriv_eq_slope

[Yury G. Kudryashov]

It would be nice to add a real_inner_product instance on [fintype ι] ι → real.

[Yury G. Kudryashov]

May be under a type tag

[Yury G. Kudryashov]

Then claim Cauchy-Schwarz inequality

[Reid Barton]

Really, I wish we had a new list of 100 theorems (or fewer would be fine, if each one is more substantial).

[Patrick Massot]

I think that list that Rocky and Ryan are currently translating is already much better

[Patrick Massot]

But it covers only undergraduate math

[Jalex Stark]

seems like a good property for a list which is meant to appeal to non-experts?

[Patrick Massot]

Yes and no. There are a couple of things that are appealing to non-expert like Fermat-Wiles

[Patrick Massot]

But those tend not to be formalized

[Johan Commelin]

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/100.yaml
Please add new data to this :up: file

[Johan Commelin]

Yury G. Kudryashov said:

The Mean Value Theorem: exists_deriv_eq_slope

Added

[Johan Commelin]

@Bhavik Mehta Didn't you add something that was on this list?

[Bryan Gin-ge Chen]

The 3 backticks here look like a copy+paste error, possibly?

[Johan Commelin]

Yup, the data wasn't very structured. I turned it into yaml using vim command recordings. Sometimes something slipped through

[Rob Lewis]

For linkifying, you should try to make sure the declaration names have the full namespace.

[Patrick Massot]

I confirm this is what it looks like

[Patrick Massot]

And I also wanted to write Rob's message

[Johan Commelin]

Rob Lewis said:

For linkifying, you should try to make sure the declaration names have the full namespace.

Yup. I hoped to crowdsource that part (-;

[Johan Commelin]

Bryan Gin-ge Chen said:

The 3 backticks here look like a copy+paste error, possibly?

They are gone now

[Jalex Stark]

so we want to put links to the appropriate files in mathlib?

[Johan Commelin]

No... rather full declaration names

[Johan Commelin]

That is likely more stable

[Johan Commelin]

Currently we have only the last bit of the name, but not the namespace

[Jalex Stark]

so we want a string that if you are in a project that depends on mathlib, and you type this string, it will either tell you that you are missing imports or will show you the theorem?

[Patrick Massot]

I think the references in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml are better: they are easy to transform to links to the dosc API, which contains links to code

[Patrick Massot]

And they are easy to check automatically

[Johan Commelin]

If you do

import all

#print some.cool.theorem_name

Then you should get a result.

[Johan Commelin]

Aah, ok. Let's do what @Patrick Massot suggests

[Johan Commelin]

Of course, if we move code and/or files, this breaks. But that shouldn't happen too often

[Patrick Massot]

This can be monitored by CI

[Rob Lewis]

The doc gen tool keeps a map from declaration name to file name (and line number). So from a full identifier you can predict its link in the html docs and the GH source. The map isn't exposed right now, but it can be if/when needed.

[Jalex Stark]

so is this the string we want to attach to #22?
data/real/cardinality.html#cardinal.not_countable_real

[Johan Commelin]

Lol, we should explain the linkifier about freek#22

[Jalex Stark]

(Johan, I'm not following what you just said; I don't know if I was meant to)

[Patrick Massot]

I would say yes to both questions

[Johan Commelin]

https://leanprover-community.github.io/mathlib_docs/data/real/cardinality.html#cardinal.not_countable_real

[Johan Commelin]

And then chop of the base URL

[Patrick Massot]

Johan meant you created a link to the 22nd issue of mathlib

[Patrick Massot]

Johan, this is what Jalex did

[Jalex Stark]

is the point that there's later some magic that will add back in the base url?

[Jalex Stark]

so someone could click it to go to the theorem statement?

[Johan Commelin]

Yup

[Jalex Stark]

Okay, I'll spend the next half hour or so putting the declarations that already exist into that format, and then submit as a PR

[Patrick Massot]

Thanks!

[Johan Commelin]

Great!

[Johan Commelin]

I don't know yaml that well

[Johan Commelin]

Sometimes we want multiple entries for a decl, so I put them in what I thought was a list.

[Johan Commelin]

Maybe this means we have to put [...] around every entry

[Johan Commelin]

But that's nothing a regex couldn't do

[Patrick Massot]

The magic of YaML is there is not much to know

[Jalex Stark]

"""
We couldn’t find any code matching 'sqrt_two' in leanprover-community/mathlib
"""

[Jalex Stark]

(I guess in my first pass I'll just PR the theorems for which the existing declaration can be found in mathlib by searching its name, which I suspect is most of them)

[Jalex Stark]

Johan Commelin said:

If you do

import all

#print some.cool.theorem_name

Then you should get a result.

is there literally a thing called import all?

[Bryan Gin-ge Chen]

You can generate src/all.lean by running scripts/mk_all.sh .

[Yury G. Kudryashov]

It's irrational_sqrt_two

[Yury G. Kudryashov]

in data.real.irrational

[Jalex Stark]

I think I made a PR
https://github.com/leanprover-community/leanprover-community.github.io/pull/16

[Johan Commelin]

@Jalex Stark Great! I left a little comment. Thanks for the effort!

[Jalex Stark]

so I'm at the PR page and I want to make further edits to the file, but i haven't figured out how yet

[Johan Commelin]

@Jalex Stark You have a branch?

[Yury G. Kudryashov]

Now it parses to this JSON (see below). Probably we should remove all "- ".

{
  "100thms": {
    "1": [
      {
        "title": "The Irrationality of the Square Root of 2"
      },
      {
        "decl": "data/real/irrational.html#irrational_sqrt_two"
      },
      {
        "author": "mathlib"
      }
    ],
    "2": [
      {
        "title": "Fundamental Theorem of Algebra"
      },
      {
        "decl": "analysis/complex/polynomial.html#complex.exists_root"
      },
      {
        "author": "Chris Hughes"
      }
    ]
  }
}

[Jalex Stark]

Johan Commelin said:

Jalex Stark You have a branch?

I don't know; i made the PR link by clicking buttons in the github web client

[Johan Commelin]

@Jalex Stark How did you create the PR? Completely on Github? Or did you work with a local git clone of the repo?

[Johan Commelin]

Aha

[Johan Commelin]

The easiest thing would be to git clone the repo, and then git checkout khanh93:patch-1

[Johan Commelin]

That's the branch that github created for you

[Johan Commelin]

After that, just edit the file, git commit, git push, and you're done.

[Jalex Stark]

okay, i'll try that

[Johan Commelin]

@Yury G. Kudryashov Are you suggesting we switch to json?

[Yury G. Kudryashov]

No, I wanted to show the effect of using "- "

[Yury G. Kudryashov]

I suggest we use

---
100thms:
  '1':
    title: The Irrationality of the Square Root of 2
    decl: data/real/irrational.html#irrational_sqrt_two
    author: mathlib
  '2':
    title: Fundamental Theorem of Algebra
    decl: analysis/complex/polynomial.html#complex.exists_root
    author: Chris Hughes

[Johan Commelin]

/me doesn't know yaml

[Johan Commelin]

@Yury G. Kudryashov What should we do with multiple decls?

[Johan Commelin]

Put them in a list? What is the idiomatic yaml solution?

[Yury G. Kudryashov]

I don't know what is the idiomatic yaml solution.

[Yury G. Kudryashov]

I'd put then in a list

[Yury G. Kudryashov]

Either using

decl: [decl1, decl2]

or using

decl:
  - decl1
  - decl2

[Johan Commelin]

I think 2 is better, unless we like long lines

[Yury G. Kudryashov]

Both parse to the same data structure

[Jalex Stark]

Johan Commelin said:

The easiest thing would be to git clone the repo, and then git checkout khanh93:patch-1

I did git clone <appropriate url> and then cd leanprover-community.github.io/ but git checkout khanh93:patch-1 resulted in error error: pathspec 'khanh93:patch-1' did not match any file(s) known to git
Probably my confusion will dissolve if I leave this alone for a day and then do a close read of e.g. the tutorial we link to from the "contribute to mathlib" page

[Johan Commelin]

O.o.... now I'm confused

[Johan Commelin]

What does git branch say?

[Jalex Stark]

* newsite

[Johan Commelin]

Hmm, so it didn't download your branch

[Johan Commelin]

git fetch origin?

[Patrick Massot]

Why does this newsite branch still exist?

[Jalex Stark]

Johan Commelin said:

git fetch origin?

gave no errors and no output

[Johan Commelin]

O.o... @Jalex Stark I gave bad advice

[Johan Commelin]

Apparently github forked the repo for you

[Patrick Massot]

Oh I see

[Johan Commelin]

https://github.com/khanh93/leanprover-community.github.io/tree/patch-1

[Patrick Massot]

This is because ofgithub pages requirements

[Johan Commelin]

So it is branch patch-1 in another repo

[Jalex Stark]

okay

[Johan Commelin]

So git remote -v

[Jalex Stark]

you made a comment that was also a suggested edit, how did you do that?

[Johan Commelin]

And then git remote add where you change leanprover-community into khanh93

[Johan Commelin]

Jalex Stark said:

you made a comment that was also a suggested edit, how did you do that?

Through the github interface

[Jalex Stark]

do you know which buttons you pressed?

[Johan Commelin]

If you go to "Changed files" on the PR page, you can click on a line, leave a comment, and there is a button for "Suggestions"

[Johan Commelin]

image.png

[Johan Commelin]

It's the first icon in the toolbar of the comment window

[Jalex Stark]

nice, thanks

[Jalex Stark]

it does in fact say "insert a suggestion" when you mouse over it, so I should have found it on my own... I just kind of enter a panic whenever I have to interact with github

[Jalex Stark]

Okay, I think it's in a state where if I walk away from it, it will soon either get accepted or someone will raise another issue?

[Johan Commelin]

@Jalex Stark I've merged it. We can convert to Yury's format in a next step.

[Jalex Stark]

Does "merged" imply that I should now treat the PR page as an archive?

[Jalex Stark]

like if I wanted to make more similar edits, I would open a new one?

[Jalex Stark]

(I don't have any similar edits right now, otherwise they would have made it into the one you just merged :slight_smile: )

[Reid Barton]

Yes

[Johan Commelin]

@Jalex Stark And next time, feel free to start a branch on the main repo. You should have the rights to do that (-;
It doesn't matter too much, unless it's collaborative, because then others can also push to the branch.

[Ryan Lahfa]

Johan Commelin said:

Yury G. Kudryashov Are you suggesting we switch to json?

YAML is a superset of JSON
so technically, a JSON file is a YAML, I have used this trick many times in my life

[Bhavik Mehta]

I added infinite ramsey, it's currently in the extras branch of my combi project

[Bhavik Mehta]

I haven't PR'd to mathlib because it depends on Reid's crec

[Johan Commelin]

Aha, I see

[Mario Carneiro]

crec should be in mathlib

[Bhavik Mehta]

Okay, where should it go? And can someone help me document it?

[Kevin Buzzard]

Patrick Massot said:

Ridiculous indeed

Just reading this thread now, but I talked to Freek about the issue of the list being poorly-specified and he said that it was not poorly specified as far as a mathematician was concerned (we all know what the triangle inequality is, even if we all think it means different things). He made it clear that it was a design decision not to formally specify anything, because he did not want to put words into formalisers heads. This example with S-vK is perhaps a neat summary of the consequences of this.

[Jalex Stark]

I guess that means people should care about what the statements look like in different ITPs, and not just the number of statements proved

[Reid Barton]

Well, there's a difference between formally specifying things and writing an informal statement of what the theorem is supposed to be

[Jalex Stark]

well freek did that, it's just very informal. In particular, there are theorems which if proven in an ITP, one can go ahead and say "yeah that satisfies the description freek gave", and who cares if there are more than one such theorem.

[Mario Carneiro]

I'm actually impressed that he has managed to interact with so many theorem proving communities and still retain his connection to mathematical vaguery. I would absolutely be tempted to give something very close to formal statements for these if I were in his position

[Kevin Buzzard]

Yeah but the moment you say set or type you're making implicit foundational assumptions. I think Freek was very smart to stay out of this business and to write something which mathematicians could read

[Jalex Stark]

Johan Commelin said:

Jalex Stark And next time, feel free to start a branch on the main repo. You should have the rights to do that (-;
It doesn't matter too much, unless it's collaborative, because then others can also push to the branch.

I'm sorry I need so much handholding. What does it mean to start a branch on the main repo? As far as I can tell it means that I have to replace step 1 of this instruction set with something else. Will I then be able to follow the rest of it normally?

[Johan Commelin]

You can replace the first 3 bullet points with "Clone mathlib"

[Johan Commelin]

After that

cd mathlib/
git checkout -b my-cool-branch
# do some changes
git add foo bar quux more stuff
git commit
git push
# this will tell you that you need to set a tracking branch or something
# just execute the command that it gives you

[Johan Commelin]

After that, it will even give you back a URL to start the PR (-;

[Johan Commelin]

Maybe we should put this somewhere in a little doc

[Johan Commelin]

But the workflow only works after someone gave you write access to the repo. (Which you got somewhere last week, I think.)

[Jalex Stark]

okay so after cloning mathlib and checkouting my branch, I make a .lean file
VSCode complains about "leanpkg.path does not exist"
I'm obviously supposed to do something with the elan toolchain

[Jalex Stark]

VSCode is suggesting leanpkg configure but I'm worried that's wrong

[Bryan Gin-ge Chen]

You should be using leanproject for some of these steps.

[Jalex Stark]

Johan Commelin said:

You can replace the first 3 bullet points with "Clone mathlib"

okay, so I think I misinterpreted "clone mathlib" as "run git clone <url i get from visiting mathlib page>"

[Jalex Stark]

does someone have a better interpretation of "clone mathlib"?

[Bryan Gin-ge Chen]

That works, but you'll still want to use leanproject to get olean files, and I think leanproject will also create a leanpkg.path file.

[Jalex Stark]

okay, so let's say we're adding to the beginning of Johan's list of steps

[Bryan Gin-ge Chen]

From where you're at, leanpkg configure should be fine, then leanproject get-mathlib-cache will help you avoid having to build mathlib yourself.

[Jalex Stark]

is git clone blah first?

[Jalex Stark]

I think it's probably more useful to forget where I'm at, especially since I'm likely to misreport it. We want a set of instructions that if exactly followed, allow one to do the "make a branch of mathlib" style of development

[Johan Commelin]

Maybe it should be leanproject get mathlib

[Bryan Gin-ge Chen]

Yeah, leanproject get mathlib would replace "clone mathlib".

[Johan Commelin]

It's too long ago, since I did this...

[Jalex Stark]

does that mean you do this only once?

[Jalex Stark]

and then somehow keep your branch up-to-date or something?

[Bryan Gin-ge Chen]

Yeah, pretty much. We should add a "Working on mathlib" section to the project page.

[Jalex Stark]

sure, I think we are currently interactively writing part of it

[Bryan Gin-ge Chen]

git pull, git fetch, git merge are all you need to keep your branch up-to-date (as well as git checkout if you're switching between different branches). (Plus leanproject get-mathlib-cache or the git hooks to fetch oleans all the time).

[Johan Commelin]

Right, once you have mathlib/ set up, you just create 1001 branches in it.

[Jalex Stark]

so i did leanproject get mathlib

[Jalex Stark]

do we think that I'm ready to check out a branch?

[Johan Commelin]

cd mathlib/

[Johan Commelin]

And then git checkout -b my-first-branch

[Jalex Stark]

right, thanks, I am mixing layers of abstraction

[Johan Commelin]

nvm

[Jalex Stark]

?

[Johan Commelin]

never mind. I understand the mixing

[Johan Commelin]

Anyway, you have a branch now?

[Jalex Stark]

oh okay, I still think it was bad of me to do such mixing, we will want to write a literally correct sequence of terminal commands in the article

[Patrick Stevens]

(Remember that one of the keys to git is liberal usage of git status to see what state your repository is currently in and what branch you're on)

[Patrick Stevens]

(easy to get confused if you don't keep on making the computer tell you what state you're in)

[Jalex Stark]

git status told me this

On branch freek-42
nothing to commit, working tree clean

how should I interpret it?

[Jalex Stark]

that I have a clean copy of mathlib waiting for edits to be made to it?

[Patrick Stevens]

That means you're successfully switched to the branch freek-42 and that your repo contains no diffs

[Johan Commelin]

So now mkdir -p archive/100/42

[Johan Commelin]

And then add your files in that folder

[Johan Commelin]

Then git add archive/100/42/*

[Johan Commelin]

@Jalex Stark One important thing: do you like editors in the terminal, like vim, nano, or emacs?

[Jalex Stark]

i am passably competent with emacs but prefer using Sublime and VSCode

[Bryan Gin-ge Chen]

I know it's a bit daunting to read a whole book, but I really recommend the git book for wrapping your head around git.

[Patrick Stevens]

A nontrivial proportion of my day job is handholding quant-finance researchers through git, I'm happy to answer large numbers of stupid questions if you have them

[Johan Commelin]

Because git commit might open vim for you, and then https://stackoverflow.com/questions/11828270/how-do-i-exit-the-vim-editor will contain a wealth of information on just how to get out of it.

[Johan Commelin]

git config --global core.editor "emacs"

[Bryan Gin-ge Chen]

The git interface in VS Code is pretty intuitive, though sometimes you still have to push from the command line.

[Johan Commelin]

It's only for writing < 10 lines of commit message, usually only 1 line.

[Johan Commelin]

So if you know emacs, you'll probably want that as your editor on the command line

[Jalex Stark]

Patrick Stevens said:

A nontrivial proportion of my day job is handholding quant-finance researchers through git, I'm happy to answer large numbers of stupid questions if you have them

amazing, in my job as a quant-finance researcher we use mercurial, and i've had people handhold me through how to use it enough times that I'm now just thoroughly embarrassed to ask for more help
so i don't write work code that ends up in repos anymore

[Johan Commelin]

and here you are... adding freek-42 to a repo...

[Alex J. Best]

I just made https://github.com/leanprover-community/leanprover-community.github.io/pull/19 to try and display the data in a more pretty way, comments(/help) welcome, especially with respect to how we format lists of links and decls, and how to automatically find the doc link from a decl like "inclusion_exclusion"

[Alex J. Best]

Also I feel we should add more attribution of the form mathlib (Person who committed the theorem) rather than simply mathlib

[Jalex Stark]

(i forked the conversation about developing on a branch of mathlib to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/learning.20to.20branch/near/197731335)

[Mario Carneiro]

I think mathlib attribution means "lost to time"

[Reid Barton]

From 1 to 3 levels of nesting might be excessive; how about freek-100/82_cubing_a_cube.lean?

[Reid Barton]

If we actually want multiple files, we could then create a directory (same way we do in mathlib itself)

[Mario Carneiro]

BTW I don't think freek gets the credit for the list of theorems, as his page will tell you

[Mario Carneiro]

Where is there three levels of nesting? I proposed archive/100/thm.lean naming

[Jalex Stark]

Reid Barton said:

If we actually want multiple files, we could then create a directory (same way we do in mathlib itself)

thanks, I think this is the convention i was missing

[Jalex Stark]

Mario Carneiro said:

Where is there three levels of nesting? I proposed archive/100/thm.lean naming

I proposed something worse in my git status messages

[Jalex Stark]

I think it's nice to have the theorem number

[Mario Carneiro]

Those can show up in the yaml file, md docs and in the module doc for the file

[Jalex Stark]

Mario Carneiro said:

BTW I don't think freek gets the credit for the list of theorems, as his page will tell you

hmm okay, but from a sociological point of view, the only reason we care about writing up proofs of these theorems is because freek has a popular webpage about them, and he puts in maintenance work

[Mario Carneiro]

but I expect this folder is not going to contain 100 files because many of them are in mathlib proper

[Jalex Stark]

i'd be happy with any folder name that is significantly more informative than "100"

[Mario Carneiro]

at least based on what I have seen elsewhere this is usually called the "100 theorems list"

[Reid Barton]

100theorems seems fine to me

[Mario Carneiro]

You probably won't need more than one file per theorem. If the proof is large enough to require multiple files then the supporting work should probably be in mathlib

[Jalex Stark]

yeah that seems true

[Reid Barton]

Agreed, I just wanted to leave an out for odd cases (e.g., imagine the cube dissection proof was a lot bigger, or something)

[Jalex Stark]

so i guess i should not call my thing 42_dumb_name but instead think harder and call it smart_name?

[Mario Carneiro]

All the theorems in Freek's list have actual names

[Mario Carneiro]

I suspect that's part of the eligibility criterion to be frank

[Jalex Stark]

ah, nice
I'll go with sum_of_the_reciprocals_of_the_triangular_numbers.lean for now

[Reid Barton]

I kind of like including the number, but I think it's also fine without given that we're maintaining that list (which also includes entries for the ones in mathlib proper). Was that the question?

[Jalex Stark]

i want consistency across files in whether they're numbered or not

[Jalex Stark]

so since we think not-numbering is okay, and there is already a not-numbered contribution, I think we should not-number

[Jalex Stark]

(but I like numbering and wish that there wasn't an argument against it)

[Reid Barton]

Well you're moving the file anyways

[Bryan Gin-ge Chen]

What's the argument against numbering? I also think numbers in the filenames would be useful.

[Bryan Gin-ge Chen]

(side thought: 2 digits should be fine, since 100 is Descartes's rule of signs which presumably would be in mathlib proper)

[Mario Carneiro]

I think numbers would be okay but I don't want to imply that all numbers should exist

[Mario Carneiro]

because the folder is actually only for "orphaned" 100 theorems

[Jalex Stark]

if all the numbers existed (and many of them were just one import and one theorem statement whose proof was a reference to mathlib), then instead of a separately-maintained yaml, we could just have the docs page

[Reid Barton]

We should probably also add to that directory a readme pointing at the list in the docs though, otherwise people might think these are all we have.

[Mario Carneiro]

You could do that with a single file, with mod comments for description, but if it's a folder then the organization in mathlib docs will not be great

[Jalex Stark]

that makes sense

[Jalex Stark]

and at that point there's no sense having files for theorems-already-in-mathlib

[Mario Carneiro]

I thought that the readme in the directory was the index?

[Jalex Stark]

the readme in which directory?

[Mario Carneiro]

I'm not sure exactly how the yaml turns into something human readable

[Mario Carneiro]

the archive/100theorems directory

[Mario Carneiro]

it seems reasonable to put the yaml file there

[Jalex Stark]

that makes sense

[Jalex Stark]

where is it living now?

[Mario Carneiro]

and then there is documentation overlap with the readme.md file

[Bryan Gin-ge Chen]

There's a PR to build an HTML file from the YAML here.

[Mario Carneiro]

could the PR also build the readme.md file?

[Mario Carneiro]

I don't know if I want to write markdown in a yaml file though

[Bryan Gin-ge Chen]

It could, we should settle on one place for it though. Either the community website with all the other former "extra" docs, or in mathlib where it might be a bit out of place.

[Mario Carneiro]

I suppose it could be a template like 100.html

[Mario Carneiro]

Maybe the simpler solution would be to have the readme.md just be a link to 100.html

[Alex J. Best]

Mario Carneiro said:

I think mathlib attribution means "lost to time"

That's not true in the current file though, some things such as MVT were added very recently but only say mathlib rather than Yury! AM-GM is also recent

[Yury G. Kudryashov]

AM-GM is also recent

And is also contributed by me.

[Yury G. Kudryashov]

Do we have a page that displays information from 100.yaml?

[Johan Commelin]

Not yet, I think

[Bryan Gin-ge Chen]

See https://github.com/leanprover-community/leanprover-community.github.io/pull/19

[Yury G. Kudryashov]

Fixed some issues with this PR. I'm going to merge it and fix the rest later. I think this is OK because we have no links pointing to the new page.

[Alex J. Best]

Cool thanks, that sounds good.

[Yury G. Kudryashov]

Merged, fixing compile.

[Yury G. Kudryashov]

It seems that we shouldn't use import markdown

[Rob Lewis]

Oh, I noticed that the other day, sorry I forgot to comment. markdown is a new dependency. Should probably use whatever markdown compiler the rest of the site generator is using.

[Alex J. Best]

Ah mistletoe, I missed that thanks

[Alex J. Best]

I can push the fix now

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Already fixed

[Yury G. Kudryashov]

Who will tell Freek about the update?

[Rob Lewis]

It would be nice if we went through the items on this list and made sure the declarations had nice doc strings. I just clicked on the quadratic reciprocity link. It leads to a page in the docs where the interesting result looks completely unremarkable, heh.

[Yury G. Kudryashov]

And our old list had all the statements.

[Rob Lewis]

The inception version of this project: give the current yaml file to the doc gen tool. It can find the theorem statements and doc strings and create a new yaml for the website generator.

[Alex J. Best]

Yeah for quadratic reciprocity its probably better to link to the file rather than the specific theorem, but maybe linking to the file under links and leave the decl as it is.

[Yury G. Kudryashov]

Do we have jinja+markdown on this website?

[Yury G. Kudryashov]

I mean, can I write a template in markdown with jinja?

[Yury G. Kudryashov]

I had I added https://leanprover-community.github.io/100-missing.html

[Kevin Buzzard]

The Prime Number Theorem might be feasible if someone figures how to make Mario's translation from MetaMath be about Lean reals and Lean primes...

[Alex J. Best]

Triangle inequality is a little ill defined but clearly there to some extent, possibly we should link to the definition of metric space and the fact that $\mathbf R^n$ with the 2-norm is a metric space?

[Kevin Buzzard]

Many are all a bit ill-defined -- did you see the discussion about other formalisations of this in the other provers? At least one just links to the definition of an ordered abelian group or something :-)

[Alex J. Best]

Ah I missed that discussion, but yeah I noticed that the other provers interpret this in wildly different ways.

[Yury G. Kudryashov]

We don't have an instance [fintype n] inner_product_space (n → real)

[Yury G. Kudryashov]

It should be very easy to add this, probably under some type tag because we already have a normed_space instance.

[Mario Carneiro]

Kevin Buzzard said:

The Prime Number Theorem might be feasible if someone figures how to make Mario's translation from MetaMath be about Lean reals and Lean primes...

What is actually needed is a proof that the reals are unique up to isomorphism. I already have a proof that primes are primes, this is how Dirichlet works

[Mario Carneiro]

that is, this is library work, it has nothing to do with metamath or interacting with the translated metamath library

[Jalex Stark]

What properties are we starting from to characterize the reals? This wikpedia page gives a few different paths
https://en.wikipedia.org/wiki/Real_closed_field

[Alex J. Best]

Mario Carneiro said:

In this case, the reals are plenty overdetermined

@Jalex Stark see this discussion

[Jalex Stark]

okay, thanks. I guess the answer is "assume whatever you want, and then we can pare down the assumptions if necessary but we probably won't need to"

[Alex J. Best]

Yeah, complete ordered archimidean field seems a reasonable triple of conditions though.

[Joseph Myers]

I have that instance (actually in the form inner_product_space (fin n → ℝ) rather than for a general fintype) in my definition of Euclidean spaces (along with versions of 4: Pythagorean Theorem, 65: Isosceles Triangle Theorem and 94: The Law of Cosines, as none of those require building up any nontrivial geometry beyond the inner product). It will take a few more PRs after #2720 to get that into mathlib.

[Jalex Stark]

Joseph, you can probably also knock out 27:sum of the angles of a triangle with the same technology

[Alex J. Best]

@Joseph Myers You should totally add these to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/100.yaml even if they aren't yet in mathlib, several results there already are on different repos.

[Yury G. Kudryashov]

Just use links: instead of decl:

[Yury G. Kudryashov]

Another low hanging fruit is "55: Product of Segments of Chords". E.g.,

theorem product_of_chords {E : Type*} [inner_product_space E] (x y z : E) (c r : real) (hc : y + c \bu z ∈ sphere x r) :
  ∃ c' : real, y + c' \bu z ∈ sphere x r ∧ c * c' * (norm z)^2 = (dist y x)^2 - r^2 := sorry

almost immediately follows from Vieta_formula_quadratic. Probably you'll want to reformulate it for an affine space over E.

[Patrick Massot]

Basically this list is full of elementary geometry theorems that are all low hanging fruits if you start from linear algebra instead of starting with a version of Euclid's axioms.

[Kevin Buzzard]

@Joseph Myers how far are we from Olympiad geometry?

[Joseph Myers]

I think we're a long way from being able to do formal versions of most synthetic Euclidean olympiad geometry proofs. (My formalisation of Euclidean spaces comes from trying to formalise a paper with one problem in each of the four olympiad subject areas - algebra, combinatorics, geometry, number theory - but the geometry problem on that paper doesn't actually involve that much synthetic geometry.)

There's no written IMO syllabus, but the IMO Compendium has a list of 171 "Basic Concepts and Facts" that probably includes many of the results and definitions most likely to be used in solving olympiad problems. 66 of those are geometry (and of those 66, mathlib only has a few trigonometric identities right now). (Another 23 are graph theory, so also missing from mathlib. I think mathlib is doing better on the results and definitions from that list that are neither geometry nor graph theory, though it certainly doesn't have full coverage of them.) There are of course many more geometry results that might sometimes be useful (see e.g. Evan Chen's book Euclidean Geometry in Mathematical Olympiads).

But there must also be hundreds of trivial lemmas that don't even get mentioned in olympiad proofs but are needed when formalising them, whenever you need to prove something that's obvious from a diagram (these two lines can't be parallel, these two points can't be the same, this point must be between these other two points, etc.). I'm not sure there's any good way to find those lemmas other than for someone (not me!) to try formalising synthetic solutions to a large number of problems, adding any such lemmas to mathlib along the way.

[Kevin Buzzard]

Yes, I agree that getting someone to formalise a bunch of geometry problems might be the way forward. Of course I have all Chris Bradley's old geometry example sheets and handourts -- unfortunately they're all in my office, which is inaccessible currently. I might try and get undergrads doing this. Is there some online resource for the basic stuff?

[Jalex Stark]

I think i have heard that groebner basis methods are a useful tool in automating synthetic geometry proofs? but i don't know anything about the algebraic geometry required to make the link

[Joseph Myers]

They're good for coordinate proofs. I suspect for many problems you'll run into fiddly configuration-dependence issues (need to prove that lines intersect rather than being parallel, need to prove something is an internal rather than an external bisector, etc.) before a reduction to proving a polynomial is in an ideal actually solves the original problem statement.

[Joseph Myers]

There must be plenty of online resources for basic olympiad geometry, but I don't know which are good.

[Jalex Stark]

okay, so the many small synthetic geometry lemmas we're talking about are required even for the reduction to coordinate geometry?

[Joseph Myers]

Reduction to coordinate geometry probably doesn't need them. But the coordinate statement of the problem will typically involve inequalities (when a problem says "triangle" it doesn't include degenerate triangles, when it says "circle" radius 0 isn't valid, when it says "intersect" it doesn't mean at infinity, when it says "incentre" it doesn't mean "excentre", etc.). And while Tarski's theorem says a coordinate formulation with inequalities is decidable (the first-order theory of real-closed fields is complete), deciding problems with inequalities is much harder in practice than deciding polynomial membership of an ideal using Gröbner bases. (You could get lucky if the conclusion you're asked to prove doesn't implicitly involve any inequalities and doesn't depend on any inequalities from the hypotheses. In theory even then things might not work, because it's possible the polynomial equations might only imply the polynomial result over the reals but not the complex numbers and the Nullstellensatz requires an algebraically closed field, but in practice that's unlikely to be a problem.)

[Kevin Buzzard]

My impression is that in Coq several of these things have been tried, the most successful in practice being the "area method", which is fast but isn't guaranteed to solve everything. On the other hand the Tarski algorithm is very slow

[Yury G. Kudryashov]

If someone will write definition/proofs for basic theorems about points, lines, angles, and circles, then I can participate in building advanced theorems from them using olympiad geometry style proofs.

[Yury G. Kudryashov]

I think that the basics should be done based on linear algebra because this way they're not completely useless for the rest of the library.

[Yury G. Kudryashov]

Then someone can separately prove that some sort of Euclid's axioms imply equivalence to $\mathbb R^2$.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

Yes, I agree that getting someone to formalise a bunch of geometry problems might be the way forward. Of course I have all Chris Bradley's old geometry example sheets and handourts -- unfortunately they're all in my office, which is inaccessible currently. I might try and get undergrads doing this. Is there some online resource for the basic stuff?

Yury G. Kudryashov said:

If someone will write definition/proofs for basic theorems about points, lines, angles, and circles, then I can participate in building advanced theorems from them using olympiad geometry style proofs.

I've been Leaning for a few months and am happy to slog through and formalize foundational geometry. Let me know if you find materials that would be applicable, or if anyone else also wants to work on this!

[Jalex Stark]

materials? like idk euclid's elements? or the book of problems by evan chen linked earlier in the thread?

[Jalex Stark]

are you looking for a body of desired applications that tells you what the API should be?

[Jalex Stark]

the first ten lines of code are worth a lot more than a few paragraphs saying you want to work on the problem :P

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

are you looking for a body of desired applications that tells you what the API should be?

My impression was @Kevin Buzzard was suggesting that following a set of class problems could be a good starting place for the API.

Jalex Stark said:

the first ten lines of code are worth a lot more than a few paragraphs saying you want to work on the problem :P

You're right that I don't need that to actually start doing this haha

[Jalex Stark]

Here's something close to a formally-specified problem:
define the "angle" for an ordered triple of points via the cosine / dot-product formula,
then prove that the following two definitions of "triangle ABC is isoceles" are equivalent:

• angle A B C = angle A C B
• distance A B = distance A C

[Jalex Stark]

you should consider it a success if (after trying for 5 or 20 minutes) you realize that adding more basic definitions or doing some easier exercise first would be better

[Jalex Stark]

ROCKY KAMEN-RUBIO said:

My impression was Kevin Buzzard was suggesting that following a set of class problems could be a good starting place for the API.

oops I sure am good at ignoring quoted text

[Yury G. Kudryashov]

Note that @Joseph Myers already started coding this, see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/freek.2Eyaml/near/197991545

[Yury G. Kudryashov]

So @ROCKY KAMEN-RUBIO if you want to participate, then coordinate with Joseph, please.

[Yury G. Kudryashov]

I know a few very good sources of geometry problems but they're in Russian.

[Aaron Anderson]

Are Hilbert's or Tarski's axioms of Euclidean geometry enough to practically prove Olympiad problems if you define some higher-level concepts on top of them?

[Jalex Stark]

I think the answer has to be yes if the problems are definable from such axioms

[Reid Barton]

The key word is "practically", I think, and I don't know the answer. It seems to be a lot of work to get to that point.

[Jalex Stark]

I think the roadmap we're suggesting here is to start by showing that the real plane (together with its affine subspaces) is a model of those axioms, and then build a library of stuff that is in principle provable from those axioms, but letting yourself shortcut with coordinate-y / linear algebraic proofs of stuff where convenient

[Jalex Stark]

and the hope is to build the library that people in practice use to solve these problems

[Reid Barton]

Yes, this is a good approach, but even with such a library, there is a lot of configuration information to contend with.

[Reid Barton]

A good milestone is just to prove that every triangle has an orthocenter.

[Kevin Buzzard]

An imperial undergrad went through some textbook in 2018 which started with Tarski's axioms and built up a huge amount of theory

[Kevin Buzzard]

It is completely undocumented but it closely follows a book which IIRC is in German

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Geometry/README.md

[Kevin Buzzard]

Rocky, it would be an interesting task to work out what the heck is going on in that repo. My impression is that @Ali Sever proved a lot of stuff

[Ali Sever]

I've almost finished my detailed walkthrough of my code. It'll be up today.

[Kevin Buzzard]

I had no idea you were working on it Ali! That's great news! Euclid comes up again and again here

[Joseph Myers]

If I complete formalising the problem I'm aiming for, that will probably get the circumcentre and orthocentre (and the fact that the reflections of the circumcircle in the sides of the triangle pass through the orthocentre, or equivalently that the reflections of the orthocentre in the sides lie on the circumcircle).

[Joseph Myers]

@Jalex Stark I have the forward direction of pons asinorum, which is true for any three points. The converse requires defining "triangle" first (= 2-simplex = 3 affine-independent points, since we want definitions to be valid in n dimensions where that's sensible), it's not true for all degenerate triangles.

[Johan Commelin]

Has anyone pinged Freek so far? I think that by now we can.

[Johan Commelin]

Freek's page is still pointing to the old list. The new list https://leanprover-community.github.io/100.html has 9 items that are not on Freek's page.

[Johan Commelin]

New statements in lean: 10, 19, 31, 38, 42, 75, 78, 85, 91

[Yury G. Kudryashov]

Can we add statements to the new page?

[Johan Commelin]

What do you mean?

[Alex J. Best]

Yury G. Kudryashov said:

Can we add statements to the new page?

That sounds good to me, what were you thinking?
Formal or informal statements? Lean ones only for the completed ones in Lean?

[Yury G. Kudryashov]

I mean quoting parts of apidocs with theorem statement.

[Yury G. Kudryashov]

This would require support from doc generator

[Johan Commelin]

Ah, I see what you mean. Your not talking about adding extra entries, but improving the html file generated from the yaml.

[Yury G. Kudryashov]

Yes, the old page has formal theorem statement right there.

[Floris van Doorn]

I sent Freek an email to update the links on his page, and add the 9 new entries.

[Johan Commelin]

@Floris van Doorn Thanks

[Rob Lewis]

Yury G. Kudryashov said:

Can we add statements to the new page?

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20map/near/199969108 . The doc gen tool can export a json file with this info but there are (minor) complications right now.

[Yury G. Kudryashov]

@Floris van Doorn Freek's page still says 29, and we already have (The Answer to the Great Question Of Life, the Universe and Everything).

[Yury G. Kudryashov]

Did he answer your email?

[Kevin Buzzard]

I just prodded him

[Kevin Buzzard]

I wonder whether in future the canonical thing to do is to prod him every time we go one position higher in the all time list

[Patrick Massot]

What about doing it only every ten items?

[Mario Carneiro]

Over in metamath land we usually report one after every one or maybe two items (depending on how hard the problem is or how much we care about getting the word out). I expect Freek just missed the email; there are often long delays but nothing malicious seeming, I think he is just a typical busy academic

[Kevin Buzzard]

He replied -- indeed he's worrying about a talk

[Floris van Doorn]

He indeed didn't reply to my email yet. My experience is that he will get to it eventually.

[Floris van Doorn]

Freek replied and updated his webpage today. I will reply with the 4 new additions since last time :)

[Alex J. Best]

@Jujian Zhang do you want to add a link to your $e$ is transcendental proof to our Freek 100 theorems list ? https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/100.yaml#L206 number 67

[Jujian Zhang]

Yes, I will do that when I am home. Thank you for the link.

[Alex J. Best]

Thank you for proving it!

[Patrick Massot]

And don't forget to bring it to mathlib! This is much more important than this list.

[Joseph Myers]

Reid Barton said:

A good milestone is just to prove that every triangle has an orthocenter.

It took a while, and we're not really any closer to being able to do synthetic geometry proofs, but #3872 defines orthocenter for a triangle (in terms of the n-dimensional generalization, monge_point for a simplex), and proves basic properties (lies in the altitudes, is the unique point in any two of the altitudes, position on the Euler line in relation to O and G).

Now that I can state the answer to the geometry problem on the olympiad paper I'm formalizing (which required orthocenter), I can get onto formalizing the solution to that problem (having formalized the solutions to all the non-geometry problems on that paper some time ago).

[Johan Commelin]

@Joseph Myers Wow! Thanks a lot for your continuous stream of PRs on this topic.

[Bhavik Mehta]

For anyone interested, @Aaron Anderson and I have got a sorry-free proof of Freek 45 in a branch of mathlib, and we're in the process of making PRs

[Oliver Nash]

I was surfing our list of the Freek 100 and was a bit surprised to see we don't officially have Cramer's rule, number 97, since I know we essentially do.

[Oliver Nash]

Looking more closely though, I see all the hard work has been done but the actual statement of Cramer's rule isn't there so I guess I'll PR it. Just mentioning it unless somebody else is already on it!

[Oliver Nash]

(in which case I will refrain)

[Johan Commelin]

Go go go go go!!!