Zulip Chat Archive

Stream: condensed mathematics

Topic: blogpost


Johan Commelin (Jul 15 2022 at 15:42):

Here is a draft of a blogpost that we hope to publish really soon:

Completion of the Liquid Tensor Experiment

We are proud to announce that as of 15:46:13 (EST) on Thursday, July 14 2022 the Liquid Tensor Experiment has been completed. A year and a half after the challenge was posed by Peter Scholze we have finally formally verified the main theorem of liquid vector spaces using the Lean proof assistant. The blueprint for the project can be found here and the formalization itself is available on GitHub.

The first major milestone was announced in June last year. The achievement was described in Nature
and Quanta.

For more information about Lean and formalization of mathematics, see the Lean community website.

<!-- TEASER_END -->

The success of the project is the result of the hard work of many people in the Lean community. The project was led by Johan Commelin and relied on continuous mathematical support from Scholze himself. Adam Topaz contributed vast amounts of homological algebra and condensed mathematics.

The other people involved in the formalization effort are as follows:
Reid Barton,
Alex J. Best,
Riccardo Brasca,
Kevin Buzzard,
Yaël Dillies,
Floris van Doorn,
Fabian Glöckle,
Markus Himmel,
Heather Macbeth,
Patrick Massot,
Bhavik Mehta,
Scott Morrison,
Filippo A. E. Nuccio,
Joël Riou,
Damiano Testa,
Andrew Yang.

In addition, the following provided valuable technical assistance:
Mario Carneiro,
Bryan Gin-ge Chen,
Rob Lewis,
Yakov Pechersky,
Ben Toner,
Eric Wieser,
leanprover-community-bot.
The Liquid Tensor Experiment also heavily relied on many parts of mathlib,
the main mathematical library for the Lean proof assistant.

The project was completed at the Institute for Computational and Experimental Research in Mathematics (ICERM) during the week-long workshop Lean for the Curious Mathematician 2022. Johan Commelin was supported by a Walter Benjamin position of the Deutsche Forschungsgemeinschaft (DFG) to work on this project.
Kevin Buzzard's work in this project was partially supported by a Microsoft Research grant. The Hoskinson Center for Formal Mathematics at Carnegie Mellon University provided server support.

Anatole Dedecker (Jul 15 2022 at 15:45):

Do we really want to include leanprover-community-bot ? x)

Johan Commelin (Jul 15 2022 at 15:46):

Honourable mention (-;

Adam Topaz (Jul 15 2022 at 15:46):

We would have drowned in linting if it wasn't for the bot!

Johan Commelin (Jul 15 2022 at 15:47):

A true collaboration of humans and machines :rofl:

Riccardo Brasca (Jul 15 2022 at 15:48):

Maybe you can add a link to analytic.pdf, citing theorem 9.1 (even if it is in the readme).

Reid Barton (Jul 15 2022 at 15:49):

Or maybe even include the statement of the main theorem (like in the challenge blogpost)

Johan Commelin (Jul 15 2022 at 15:51):

Good points!

Johan Commelin (Jul 15 2022 at 17:28):

It's live: https://leanprover-community.github.io/blog/posts/lte-final/

Yakov Pechersky (Jul 15 2022 at 19:55):

Would it be possible to link the completed link to a commit that has a green check instead of the red X (because of linters)?

Adam Topaz (Jul 15 2022 at 19:59):

I think a commit message of DONE is better than chore(scripts): update nolints.txt

Yakov Pechersky (Jul 15 2022 at 20:01):

For sure. Looking at the lint log, it's actually super nice -- the aux lemmas had some unused arguments.

Yakov Pechersky (Jul 15 2022 at 20:01):

DONE'

Adam Topaz (Jul 15 2022 at 20:06):

Maybe we should leave that as is (because of the timestamp), and try eliminate the nolints over the next few weeks (months?). And when that's done, we can make a meaningful final commit message when we finish with all the nolints, and add (Update: Linting has now been done.) with a link to that commit in the blogpost.

Adam Topaz (Jul 15 2022 at 20:06):

Generic mathematicians probably have no clue what the word lint means, but that's okay :)

Adam Topaz (Jul 15 2022 at 20:07):

It would be good to add the various docstrings anyway!

Reid Barton (Jul 15 2022 at 20:08):

and don't forget to move all the for_mathlib stuff to mathlib :upside_down:

Kevin Buzzard (Jul 15 2022 at 20:10):

Just cut and paste it into a from_LTE directory maybe?

Adam Topaz (Jul 15 2022 at 20:12):

nolint.txt is only 642 lines long

Johan Commelin (Jul 15 2022 at 21:56):

I was also surprised. I expected > 1000.

Julian Berman (Jul 16 2022 at 08:56):

How does it feel Johan?

Johan Commelin (Jul 16 2022 at 09:03):

I guess by the end of today I'll have muscle pains in my face. Because I can't get rid of that huge grin :smiley:

Ben Toner (Jul 16 2022 at 09:32):

If you wanted, I could make a branch for you with the "DONE" commit rearranged to be on top (with a green check). You could set that to be the branch people see by default, while continuing to do your work on master.

Johan Commelin (Jul 16 2022 at 09:41):

@Ben Toner Thanks, that would be cool!

Johan Commelin (Jul 16 2022 at 09:41):

And while you are at it, could you change CI to check that liquid_tensor_experiment remains sorry-free?

Johan Commelin (Jul 16 2022 at 09:41):

It is currently checking this for thm95. But we can now make a stronger claim (-;

Johan Commelin (Jul 16 2022 at 09:42):

Once you are done, we'll update the blogpost.

Johan Commelin (Jul 16 2022 at 09:42):

(Maybe we'll put two links, one to the actual historical commit, and one with the nice rewritten history.)

Ben Toner (Jul 16 2022 at 10:26):

Both done. https://github.com/leanprover-community/lean-liquid/commits/completed
(Detail: this branch omits a commit of Rob that made changes on top of Adam's "DONE" commit.)

Johan Commelin (Jul 16 2022 at 10:27):

Thanks!

Johan Commelin (Jul 16 2022 at 10:27):

Those commits by Rob are actually important.

Johan Commelin (Jul 16 2022 at 10:28):

Because the clean up the statement of the main file. (Which for our target audience is probably more important than the :cross_mark: vs :check:)

Johan Commelin (Jul 16 2022 at 10:28):

So do you think you could rewrite history on that branch with some cherry-pick magic?

Ben Toner (Jul 16 2022 at 10:28):

You have the clean-up, just not this one https://github.com/leanprover-community/lean-liquid/commit/e1165e769b3a94e86011292cab6b915b42be1a80

Johan Commelin (Jul 16 2022 at 10:29):

Ooh! Ok. Gotcha

Johan Commelin (Jul 16 2022 at 10:29):

Yeah, that's just a speedup that isn't too important.

Ben Toner (Jul 16 2022 at 10:29):

i can rewrite the branch to include the missing commit, but it would involve editing Adam's "DONE" commit

Johan Commelin (Jul 16 2022 at 10:30):

No, I don't think we need this commit on the completed branch

Johan Commelin (Jul 16 2022 at 10:30):

I am about to arrive back home. I'll have lunch and some family time first. And then I'll add a pointer to this new branch.

Ben Toner (Jul 16 2022 at 12:03):

Some stats:

Number of lemmas: 3400
Number of defs: 2360
Number of theorems: 136

Counts exclude commented-out code.

Riccardo Brasca (Jul 16 2022 at 12:12):

Do you know how many lines?

Ben Toner (Jul 16 2022 at 12:14):

I'll do that shortly

Ben Toner (Jul 16 2022 at 13:07):

Number of lines: 90967
Number of nonblank lines: 78702
Number of nonblank lines excluding comments and docstrings: 72661

Johan Commelin (Jul 16 2022 at 17:38):

Ben Toner said:

Both done. https://github.com/leanprover-community/lean-liquid/commits/completed
(Detail: this branch omits a commit of Rob that made changes on top of Adam's "DONE" commit.)

I pushed a commit to the blog repo, so that the post now links to this branch. Should be live in a few minutes. Thanks again @Ben Toner


Last updated: Dec 20 2023 at 11:08 UTC