blogpost

Stream: condensed mathematics

[Johan Commelin]

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]

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

[Johan Commelin]

Honourable mention (-;

[Adam Topaz]

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

[Johan Commelin]

A true collaboration of humans and machines :rofl:

[Riccardo Brasca]

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

[Reid Barton]

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

[Johan Commelin]

Good points!

[Johan Commelin]

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

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

DONE'

[Adam Topaz]

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]

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

[Adam Topaz]

It would be good to add the various docstrings anyway!

[Reid Barton]

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

[Kevin Buzzard]

Just cut and paste it into a from_LTE directory maybe?

[Adam Topaz]

nolint.txt is only 642 lines long

[Johan Commelin]

I was also surprised. I expected > 1000.

[Julian Berman]

How does it feel Johan?

[Johan Commelin]

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]

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]

@Ben Toner Thanks, that would be cool!

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Ben Toner]

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]

Thanks!

[Johan Commelin]

Those commits by Rob are actually important.

[Johan Commelin]

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]

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

[Ben Toner]

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

[Johan Commelin]

Ooh! Ok. Gotcha

[Johan Commelin]

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

[Ben Toner]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Some stats:

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

Counts exclude commented-out code.

[Riccardo Brasca]

Do you know how many lines?

[Ben Toner]

I'll do that shortly

[Ben Toner]

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

[Johan Commelin]

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