100.yaml and the archive

Stream: general

[Johan Commelin]

Should we add support for declarations in archive/ to 100.yaml?
Some of the links in https://github.com/leanprover-community/mathlib/blob/master/docs/100.yaml are long links to the archive, and I think just listing the decl name should be enough for the script to locate it.

[Yaël Dillies]

That's a good idea!

[Yaël Dillies]

Should we also list theorems that are not on Freek's list but still worth mentioning?

[Yaël Dillies]

Also, it seems that Freek's website is a bit outdated regarding Lean's achievement. Should we email him, maybe?

[Scott Morrison]

There's also the overview pages for "still worth mentioning".

[Johan Commelin]

Yes, this list should be only Freek's list. It's a particular list, and many people are unhappy about which theorems are on it, but it has become a measuring stick for theorem provers....

[Johan Commelin]

@Yaël Dillies there are some open PRs for 100.yaml. I was thinking of pinging Freek (he's on this Zulip) after those were merged.

[Yaël Dillies]

Okay thank you both for the info!