Project completed! Thoughts and reflections?

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

As of a few minutes ago, Lean managed to prove PFR_conjecture without any sorrys. So the primary goals of this project have all been completed! Thanks to everyone (most importantly @Yaël Dillies who heroically got the project up and running in 48 hours, but also @Rémy Degenne, @Sebastien Gouezel , @Bhavik Mehta , @Heather Macbeth , @Kalle Kytölä, @Paul Lezeau , @Scott Morrison, @Mauricio Collares , @Patrick Massot , @Arend Mellendijk , @llllvvuu , @Jonas Bayer , @Floris van Doorn , @Ben Eltschig, @Mantas Baksys , @Kyle Miller , @Aaron Anderson, @Rob Lewis , and everyone else who participated - sorry if I omitted anyone by mistake) for all the contributions; this is definitely something that could not have been accomplished by just one person.

While the memories of the project are still fresh, this would be a good time for participants to make any observations and reflections on how the project proceeded, and in particular what suggestions people would have for any future projects of this type. (I don't anticipate leading another project like this in the near future, but I am sure there will be others who would like to try.) I'll start the ball rolling with some thoughts of my own.

1. I didn't anticipate that the majority of my time on the project would be spent on the math side (in particular, organizing the blueprint) and the social side (coordinating all the other contributors); I did fill in a few sorries, but I estimate that I only contributed about 5% or so of the lines of code. This is actually quite encouraging to me, as it suggests to me that it will be possible for mathematicians to lead Lean formalization projects without requiring extensive Lean programming skills (though one may need at least enough expertise to be able to state lemmas, if not prove them). (Also, given how many times I broke the build by using my administrator privileges to push updates without passing through CIs, it is perhaps for the best that I didn't do a substantial amount of coding.)

2. As with my previous formalization project, I found that the most mathematically interesting portions of the project were relatively straightforward to formalize, but it was the technical "obvious" steps that took the longest, most notably in the final stretch when we struggled to establish properties of independent random variables.

3. Blueprint works really well to break up the project into lots of chunks of small to medium difficulty, and allow for plenty of parallelization. In particular it seems that many contributors were able to work on one localized subtask without necessarily understanding the global proof (or even be in roughly the field of mathematics - additive combinatorics - that this result is in).

4. As pointed out by @Kevin Buzzard , the "outstanding tasks" thread was very useful in coordinating the project and encouraging people to contribute. I wondersif there could be some way to formalize this sort of claiming and releasing of task "tokens", perhaps through some tighter integration with Blueprint.

5. Only some very minor typos in the original paper were picked up as a consequence of the formalization project, which was reassuring (my coauthors and I did take multiple passes through the paper to check everything). There were a larger number of minor issues with the blueprint, in that certain standard hypotheses such as measurability were sometimes omitted, or the dependency tree wasn't quite described correctly, but nothing that couldn't be easily fixed.

[Johan Commelin]

I don't want to immediately hijack this thread, but I think

[...] I estimate that I only contributed about 5% or so of the lines of code.This is actually quite encouraging to me, as it suggests to me that it will be possible for mathematicians to lead Lean formalization projects without requiring extensive Lean programming skills [...]

is something that will be highly dependent on some cultural factors as well. Of course you got a lot of help with this project because of its high-profile nature, derived from the fact that the formalization target was a proof by the "A-team" resolving an open conjecture.
At the moment, it is still not clear how formalizers (for lack of a better job description) will be credited by the mathematical community, and how these activities will be valued on the job market.

I am happy to move this message to a new thread if it spawns a longer discussion.

[Mauricio Collares]

Besides the author list, it's also high-profile because the conjecture itself was a central one in the field of additive combinatorics :) This year was a good one for "Hungarian-style" combinatorics in general (exponential Ramsey, R(4,t), density of 3-AP-free sets, and PFR), and three out of the four results I mentioned are at least partially formalized in Lean. Curiously, the one that isn't, R(4,t), is the one that's already accepted for publication in the Annals, although I'm sure the other ones will appear soon :)

[Yaël Dillies]

For those not following closely:

• exponential Ramsey is formalised here
• R(4, t) is not formalised (although Bhavik now has a sizable portion of the setup ready)
• density of 3AP-free sets is halfway through formalising in LeanAPAP. The new ideas are already formalised and now I just need to power through a bunch of boring analysis
• PFR, well, you're on topic :wink:

[Rémy Degenne]

My first thought about the project (biased by my own contribution) is that in this project and in most others I am aware of, a large part of the effort is spent formalizing simple prerequisites. What is in Mathlib and what isn't is mostly driven by the specific interests of the contributors, and even though we have more and more people contributing to Mathlib it's still only a few people per mathematical area.
In this project, I think none of the 5000+ lines I have pushed to the repository have anything to do with the main part of the paper. Everything is about the entropy notions recalled in the appendix.

[Yaël Dillies]

The fact that the community is housing so many probability theory experts was instrumental, for sure!

[David Michael Roberts]

Wow, just four months for the Ramsey number bound to get through refereeing! I guess 16 pages of combinatorics, sans references and intro, makes it slightly quicker than a 100-page paper in, say, algebraic number theory...

[Shreyas Srinivas]

As an outsider looking in:

1. That seems impressively fast given the reputation that formalisation projects have for being slow and years behind the actual result.
2. About the tool, maybe something like Trello could come in handy for requesting and allowing claims. I am not aware of any tool other than SVN that can strictly enforce claims to files. But SVN comes with other disadvantages. Mainly, it needs an internet connection to work, and the setup is tedious.
3. What Johann says. What are the available career paths for math formalisation? Will this work be valued? Maybe in the future we have an institute for formalisation that employs people long term for such projects (De Bruijn Institute sounds like a good name).
4. The project quickly moved towards measure theoretic generality for probability stuff. I am curious how easy/difficult a purely discrete formalisation would, be primarily because of library support.

[Floris van Doorn]

As one of the formalisers, I was very impressed by the quality and detail in the blueprint. It is not easy to write a proof in such detail that an outsider can come in and just formalize a single lemma in the blueprint without knowing the context within the larger proof. But the detail in the blueprint was large enough to quite easily write the formal proofs (at least for a Lean expert).

[Mauricio Collares]

SVN does not enforce claims to files. Are you thinking of Visual SourceSafe?

[Shreyas Srinivas]

Yes. But there is also an SVN lock

[Mauricio Collares]

Huh, TIL

[Mauricio Collares]

But there's a reason people locked files back then: Merging was much harder. I think locking now would be a big regression in workflow.

[Shreyas Srinivas]

Version control-wise yes. The git approach is to work independently and make PRs to the main repo. Then the administrator can choose the PRs to merge.

[Shreyas Srinivas]

But if the goal is to enforce the claims mechanism to avoid duplication of work, git can't do that. SVN can.

[Terence Tao]

Johan Commelin said:

At the moment, it is still not clear how formalizers (for lack of a better job description) will be credited by the mathematical community, and how these activities will be valued on the job market.

That's a good point. For what it's worth, I'm more than happy to mention contributions to this project in letters of reference as appropriate. My co-authors and I will mention the Lean project (and link to the github) in the next revision of our paper, though I'm not sure whether it would be a good idea to explicitly name contributors to the project in the paper (there is the question of where to draw the threshold for the size of contribution which would merit mentioning the contributor). One could simply point to https://github.com/teorth/pfr/graphs/contributors , perhaps, or make a link to that page from the github front page.

Regarding the broader question of persuading the mathematical community (and funding agencies) to value formalization, I know there are plans to launch a journal centered around formalization, which should help. One could potentially imagine some way to create more quantifiable metrics for formalization contributions (I'm vaguely thinking of something either along the lines of MathOverflow reputation, or some sort of "currency" that mathematicians seeking formalizations could put out as "bounties" for various lemma proofs), but metrics don't have a good track record in this community (among other things, they are often too easy to game), so I think they would have a secondary role to play at best.

[Oliver Nash]

I hope there is a plan to migrate the appropriate material to Mathlib!

[Yaël Dillies]

Yes! I already spent two full days tidying up the prerequisites in their appropriate files (see folder Mathlib.PFR). I will add a section to the website with the files that have no PFR imports. Then the game will be to take one of those and PR its content to mathlib. Then bump PFR. Then repeat.

[Yaël Dillies]

This process is what I've been doing for LeanCamCombi and it's very efficient.

[Oliver Nash]

Excellent, thanks!

[Kevin Buzzard]

David Michael Roberts said:

Wow, just four months for the Ramsey number bound to get through refereeing! I guess 16 pages of combinatorics, sans references and intro, makes it slightly quicker than a 100-page paper in, say, algebraic number theory...

One way a modern algebraic number theory paper differs from a modern "Hungarian style combinatorics" (if we're to call it that) paper is that the combinatorics paper might have some good new ideas but be "flying relatively close to the axioms", whereas a new paper in algebraic number theory might have some good new ideas but also might crucially depend on literally thousands of pages of prior material (all the machinery developed by Grothendieck or Langlands or Deligne or Katz in the 60s/70s, perhaps all of class field theory, and then also a whole bunch of recent developments too). Somehow the very nature of the two areas is different (or has become different, perhaps for historical reasons). This doesn't mean that either area is "better" or "deeper" than the other, it just highlights the subtle and complex nature of the field. Bollobas used to tell me in Cambridge that combinatorics was a "young" subject and number theory was an "old" one.

[Michael Bucko]

Terence Tao schrieb:

3. Blueprint works really well to break up the project into lots of chunks of small to medium difficulty, and allow for plenty of parallelization. In particular it seems that many contributors were able to work on one localized subtask without necessarily understanding the global proof (or even be in roughly the field of mathematics - additive combinatorics - that this result is in).

Congratulations!! :clap:

This is huge. The fact that we can fine tune pre-trained (using unsupervised learning) text models to generate tactics given a proof state and embed states and premises into vectors means that we will soon have AI-assisted conjectures (wrote one colab myself today using ReProver). Formalizing all this work will be extremely important (collaborative math, math using natural language, re-using blueprint building blocks like legos, further fine tuning models with reinforcement learning).

The fact that many contributors were able to work on one localized subtask without necessarily understanding the global proof immediately captured my attention. It reminds me of map reduce from back in the day. With ZKP (zero-knowledge proofs), we could have more granularity related to proofs and responsibilities. With blueprint building blocks, we could have collaborative construction.

Also, perhaps LLMs will most likely learn from this human knowledge and improve their planning / reasoning skills. (and then be even better sparing partners)

I am impressed by Blueprint, too. I can imagine exploring those graphs in AR while learning math in high school.

[David Michael Roberts]

Kevin Buzzard said:

One way a modern algebraic number theory paper differs from a modern "Hungarian style combinatorics" (if we're to call it that) paper is that the combinatorics paper might have some good new ideas but be "flying relatively close to the axioms", whereas a new paper in algebraic number theory might have some good new ideas but also might crucially depend on literally thousands of pages of prior material .... This doesn't mean that either area is "better" or "deeper" than the other, it just highlights the subtle and complex nature of the field.

Oh, I totally get that. It's what I was alluding to. But we all know that papers of much less import in much more run-of-the-mill journals can often take more than four months to referee, and not because they are more subtle or longer....

[Rémy Degenne]

Another thought about the project organization: the infrastructure around the lean code was essential for smooth collaboration. The blueprint was mentioned already, but I wanted to add that CI is also very important. In a project without CI to check the build, you could change a file, have it look nice, push to the repository and not realize that you broke 10 files downstream. In this project (as in Mathlib and others) PR authors could see the build issue and fix it before merging to master, so the build on master was most often fine.

[Omar Shehab]

Terence Tao said:

As of a few minutes ago, Lean managed to prove PFR_conjecture without any sorrys. So the primary goals of this project have all been completed! Thanks to everyone for all the contributions; this is definitely something that could not have been accomplished by just one person.

While the memories of the project are still fresh, this would be a good time for participants to make any observations and reflections on how the project proceeded, and in particular what suggestions people would have for any future projects of this type. (I don't anticipate leading another project like this in the near future, but I am sure there will be others who would like to try.) I'll start the ball rolling with some thoughts of my own.

1. I didn't anticipate that the majority of my time on the project would be spent on the math side (in particular, organizing the blueprint) and the social side (coordinating all the other contributors); I did fill in a few sorries, but I estimate that I only contributed about 5% or so of the lines of code. This is actually quite encouraging to me, as it suggests to me that it will be possible for mathematicians to lead Lean formalization projects without requiring extensive Lean programming skills (though one may need at least enough expertise to be able to state lemmas, if not prove them). (Also, given how many times I broke the build by using my administrator privileges to push updates without passing through CIs, it is perhaps for the best that I didn't do a substantial amount of coding.)

2. As with my previous formalization project, I found that the most mathematically interesting portions of the project were relatively straightforward to formalize, but it was the technical "obvious" steps that took the longest, most notably in the final stretch when we struggled to establish properties of independent random variables.

3. Blueprint works really well to break up the project into lots of chunks of small to medium difficulty, and allow for plenty of parallelization. In particular it seems that many contributors were able to work on one localized subtask without necessarily understanding the global proof (or even be in roughly the field of mathematics - additive combinatorics - that this result is in).

4. As pointed out by Kevin Buzzard , the "outstanding tasks" thread was very useful in coordinating the project and encouraging people to contribute. I wondersif there could be some way to formalize this sort of claiming and releasing of task "tokens", perhaps through some tighter integration with Blueprint.

5. Only some very minor typos in the original paper were picked up as a consequence of the formalization project, which was reassuring (my coauthors and I did take multiple passes through the paper to check everything). There were a larger number of minor issues with the blueprint, in that certain standard hypotheses such as measurability were sometimes omitted, or the dependency tree wasn't quite described correctly, but nothing that couldn't be easily fixed.

Apologies for the naive question. Is there a way I can understand the wall clock time needed to execute the proving? TIA

[Terence Tao]

Floris van Doorn said:

As one of the formalisers, I was very impressed by the quality and detail in the blueprint. It is not easy to write a proof in such detail that an outsider can come in and just formalize a single lemma in the blueprint without knowing the context within the larger proof. But the detail in the blueprint was large enough to quite easily write the formal proofs (at least for a Lean expert).

I'm beginning to realize that Blueprint is, in itself, a sort of programming language (a sort of "Lean pseudocode"), except that it is compiled by humans (at the current state of AI/Lean integration, at least) rather than by computers. It does take a non-trivial effort to switch one's writing style from Standard Mathematical English/LaTeX to Blueprint/LaTeX (in particular, being more pedantic with details and dependencies), but significantly less effort than in switching from Standard Mathematical English/LaTeX to Mathlib/Lean, and this looks like a switch that many mathematicians should be able to make. (See also this quote by Birch that he programmed in a very high-level programming language called "graduate student".)

[Siddhartha Gadgil]

Terence Tao said:

Floris van Doorn said:

As one of the formalisers, I was very impressed by the quality and detail in the blueprint. It is not easy to write a proof in such detail that an outsider can come in and just formalize a single lemma in the blueprint without knowing the context within the larger proof. But the detail in the blueprint was large enough to quite easily write the formal proofs (at least for a Lean expert).

I'm beginning to realize that Blueprint is, in itself, a sort of programming language (a sort of "Lean pseudocode"), except that it is compiled by humans (at the current state of AI/Lean integration, at least) rather than by computers. It does take a non-trivial effort to switch one's writing style from Standard Mathematical English/LaTeX to Blueprint/LaTeX (in particular, being more pedantic with details and dependencies), but significantly less effort than in switching from Standard Mathematical English/LaTeX to Mathlib/Lean, and this looks like a switch that many mathematicians should be able to make. (See also this quote by Birch that he programmed in a very high-level programming language called "graduate student".)

Sounds like Blueprint/LaTeX will be a good target language for GPT-4.

[Terence Tao]

Siddhartha Gadgil said:

Sounds like Blueprint/LaTeX will be a good target language for GPT-4.

Actually, pretty much all of the translation directions (English -> Blueprint, Blueprint -> Lean, Lean -> Blueprint, Blueprint -> English, and also Lean <-> other formal languages) look appealing to me as applications of LLMs (supervised somehow by some combination of humans and formal verifiers), and significantly more feasible than direct translations English <-> Lean.

[Siddhartha Gadgil]

Terence Tao said:

Siddhartha Gadgil said:

Sounds like Blueprint/LaTeX will be a good target language for GPT-4.

Actually, pretty much all of the translation directions (English -> Blueprint, Blueprint -> Lean, Lean -> Blueprint, Blueprint -> English, and also Lean <-> other formal languages) look appealing to me as applications of LLMs (supervised somehow by some combination of humans and formal verifiers), and significantly more feasible than direct translations English <-> Lean.

In the informalization directions: Lean -> English etc GPT-4 is already very good with just instructions. To target Lean one at least needs to give examples of Lean notation in the prompt. With examples (and automation to fill in details) there is hope for the formalization directions.

[Terence Tao]

As a heads up: this project was mentioned in today's Quanta article: https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/

[Thomas Bloom]

Congratulations to everyone involved! A massive achievement.

In terms of what next, I wonder how feasible it would be to also formalise the proof of 'weak PFR over the integers' - this is implied by PFR over F_2^n as shown by Green, Manners, and Tao (Corollary 1.12 of https://arxiv.org/pdf/2306.13403.pdf), using the same entropy-baesd toolkit.

My impression is (and hopefully @Terence Tao can correct me) that this should be reasonably short given the tools developed already for the PFR proof.

[Scott Morrison]

The Quanta article seems to suggest the same thing many articles do:

Tao announced that Lean had proved the conjecture without any “sorrys” — the standard statement that appears when the computer can’t verify a certain step.

... that no humans were involved!

The paragraph much later in the article is quite good, however.

[Terence Tao]

Thomas Bloom said:

Congratulations to everyone involved! A massive achievement.

In terms of what next, I wonder how feasible it would be to also formalise the proof of 'weak PFR over the integers' - this is implied by PFR over F_2^n as shown by Green, Manners, and Tao (Corollary 1.12 of https://arxiv.org/pdf/2306.13403.pdf), using the same entropy-baesd toolkit.

My impression is (and hopefully Terence Tao can correct me) that this should be reasonably short given the tools developed already for the PFR proof.

Hmm, this could be doable - the derivation is three and a half pages in that paper, and as you say it mostly just uses the entropy tools that already are in PFR. It would be a bit more substantial though than the other extension we already implemented of getting the homomorphism version of PFR, where the argument is more like half a page when written in regular math.

If there is sufficient interest I could try to create an addendum to the blueprint for this (or if you would like to volunteer to work on the blueprint also, that would also be appreciated :). I don't want to presume though that just because so many people already donated their time to this project that they would be willing to do so indefinitely for further extensions of the project. For instance, we will shortly have a paper doing the odd characteristic case of PFR as well, and on my blog someone has contributed an argument that improves the constant in PFR from 12 to 11; both of these are certainly possible to formalize as well, but it would require nontrivial effort on both the blueprint side and the formalization side. In each of these cases the effort is much smaller than the entirety of the PFR project - each such extension can probably be done in a matter of days if we have the same level of activity and donated time as for the primary goal - but it's unclear to me whether the cost-benefit ratio is as favorable as for the primary PFR project.

[Yaël Dillies]

I certainly am willing to work on the extensions :smile: The point of formalisation is both to do a publicity stunt every time we formalise a breakthrough and being able to check proposed improvements as they come.

[Paul Lezeau]

I'd also be up for working on extensions!

[Terence Tao]

OK. Perhaps we could then have a somewhat open-ended second stage to the PFR project where we work on a few extensions, but perhaps at a reduced rate of activity and without any expectation of a "speed run".

[Thomas Bloom]

That sounds good. I am happy to provide the blueprint level proof for deducing weak PFR at some point, but I'm not able to right now. I'll start a new thread on here when I start doing so (unless anyone has already done it by that point!)

[Eric Rodriguez]

In general, I'd say that if there's a direction, many people will follow and help out with any given lean project :)

[Kevin Buzzard]

I have been thinking about how to run a big long term project; here are two comments. Firstly I asked @Utensil Song to put a new red possibility for nodes, meaning something like "this is not done and there is no LaTeX blueprint either". I think this might be useful for me; I want to use "blue" in the same way Terry was using it -- i.e. "high chance that this sorry is feasible and you might be able to do it in one or a few Lean sessions even if you haven't read the paper".

Secondly I think it might be an interesting experiment to have a github issue for each node on the graph. Issues are cheap and might be a better way of storing the status of things than Terry's thrice-weekly updates; one could perhaps even hope to have some web page where you could just look at the current status of all non-green nodes, and a way of "claiming" nodes in real time if you want to work on them. The issue could be the one source of truth about the node if we want to reduce the chances of two people working on the same thing (which did happen once in PFR).

[Scott Morrison]

It's pretty straightforward to programmatically create issues, and to add/remove/check for labels, so that could all be integrated into the dependency graph itself.

[Scott Morrison]

Shreyas above mentioned the trello tool. It might also be a good way to claim and release things. It's easy to use, has a long-standing company behind it, and has an API that would allow some automation if desired. But keeping things simple and within the existing ecosystem might be more valuable; I'm not sure.

[Terence Tao]

Kevin Buzzard said:

I have been thinking about how to run a big long term project; here are two comments. Firstly I asked Utensil Song to put a new red possibility for nodes, meaning something like "this is not done and there is no LaTeX blueprint either". I think this might be useful for me; I want to use "blue" in the same way Terry was using it -- i.e. "high chance that this sorry is feasible and you might be able to do it in one or a few Lean sessions even if you haven't read the paper".

Secondly I think it might be an interesting experiment to have a github issue for each node on the graph. Issues are cheap and might be a better way of storing the status of things than Terry's thrice-weekly updates; one could perhaps even hope to have some web page where you could just look at the current status of all non-green nodes, and a way of "claiming" nodes in real time if you want to work on them. The issue could be the one source of truth about the node if we want to reduce the chances of two people working on the same thing (which did happen once in PFR).

Using an existing and familiar tool such as github issues sounds worth trying. If the code can be updated in time, one could imagine using the extensions to the PFR projects as a test case for various blueprint experiments. I don't know if it is possible to make addons to a github issues page to allow administrators to, for instance, insert a \leanok into a blueprint proof by clicking an extra button after approving a contributor's PR resolving that proof.

Perhaps we could have a \sorry macro in blueprint in case the statement or proof of a blueprint lemma is not yet in a form acceptable to a human reader (as opposed to a Lean compiler), and add new colors to the dependency graph accordingly.

[Scott Morrison]

You can't make addons to the issues page, but you can achieve a lot using labels, or even just whether or not a pull request has been merged.

[Scott Morrison]

If there's an issue for every label, and PRs include the magic words "Resolves #347", then #347 will automatically be closed when the PR is merged, and then the dependency graph could notice that the issue has been closed and update the blueprint accordingly.

[Terence Tao]

Is PFR basically the only active example of a Blueprint in use right now? If so it would be a natural guinea pig to use for testing experimental features, particularly since the primary goal has been achieved so there is relatively little downside risk if we temporarily break Blueprint for one reason or another.

[Yaël Dillies]

There's also LeanAPAP but I'm basically the only contributor. So not great for experimentation.

[Riccardo Brasca]

We use a blueprint in the flt-regular project (also completed yesterday!).

[Shreyas Srinivas]

Scott Morrison said:

Shreyas above mentioned the trello tool. It might also be a good way to claim and release things. It's easy to use, has a long-standing company behind it, and has an API that would allow some automation if desired. But keeping things simple and within the existing ecosystem might be more valuable; I'm not sure.

It also integrates with github and has its own dependency graphs

[Terence Tao]

There is a new thread over at general https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/CFP.3A.20improved.20Blueprint.20UX about blueprint updates in a broader context than PFR.

[Yakov Pechersky]

A nice thing about Github Issues is that they are represented directly in the Github projects kanban board, without having to use something like trello.

[Utensil Song]

Terence Tao said:

Is PFR basically the only active example of a Blueprint in use right now? If so it would be a natural guinea pig to use for testing experimental features, particularly since the primary goal has been achieved so there is relatively little downside risk if we temporarily break Blueprint for one reason or another.

I have a list of the projects using Lean 4 version of leanblueprint here, and intend to keep it growing.

Lean 4 version of blueprint was initially asked for by flt-regular and LeanAPAP. With @Patrick Massot 's guidance and @Henrik Böving 's help on the side of doc-gen4, the prototype was developed using my experimental blueprint for lean-ga project (it has a lot to catch up with the work of @Eric Wieser and the initial goal) as a test bed. I set up an example project (now outdated) with the idea to make it a template for both and more projects, but the solution turns out to have too many moving parts, so @Chris Birkbeck asked me to set up directly for flt-regular then later by
@Yaël Dillies for LeanAPAP, which was the base setup for PFR by @Yaël Dillies .

During flt-regular, LeanAPAP, PFR, and with observations from @Yaël Dillies and thoughts from @Kevin Buzzard , quite a few issues were discovered and fixed, the SOTA of the fixes are mostly in PFR so PFR is the latest test bed for the development of Lean 4 version of blueprint, and due to the status quo of too many moving parts in the setup, all these projects are different in certain details and might cause confusion and frustrations for mathematicians or Lean experts if something breaks due to a change to one of the building blocks, and the fixes in PFR are not back ported to previous projects yet, that's why I drafted RFC: Absorb scattered functionalities back into leanblueprint to address this discrepancy (but haven't raised it for public discussion yet as I was drowned in work lately).

The most observable improvements of these fixes are reducing the CI time from around half an hour to 17min (if the commit doesn't update Mathlib), and a simple tool inv check to check if all blueprint \lean references do exist in the Lean code.

Moving forward, I was hoping for a new active formalization project as a test bed to further improve how the blueprint works. I'll post more thoughts in the new thread by Morph Labs later.

[Patrick Massot]

I'm a bit late to the party because I've been very busy. But I'd like to write some comments, although there is overlap with things that were already said.

This projects proves once again that it is possible to efficiently formalize non-trivial mathematics using Lean and Mathlib in their current state (which is far from what we expect to be their state in a couple of years, even without any AI dreaming).

This is great, but let's not forget that we are still very far from being able to formalize in real time. During the three weeks of this project, at least 2000 math papers appeared on arXiv (see for instance those stats). Admittedly many of those papers are probably not worth reading, even less formalizing. But there is still a factor 1000 between the formalization speed of this collaboration and the production of math papers.

Today if you are Peter Scholze or Terence Tao you can come here, launch a formalization project and instantly get 15 people working on it. It simply doesn't work otherwise. This isn't a thought experiment, we see this very often. Yesterday we also saw the completion of the FLT-regular project which obviously did not get such a rush, and the same applied for the sphere eversion project. Those two projects got completed eventually, but at a much lower speed.

We are also currently limited in the kind of mathematics we can efficiently tackle. If Scholze comes back and proposes to formalize his paper with Laurent Fargues then there won't be a miracle in three weeks (or even one year and a half as for LTE). And it isn't clear the enthusiasm would last long enough to go through a blueprint with thousands of pages.

Keeping all that in mind, the good news is that everything is improving. Mathlib gets bigger and bigger, new tactics appear every week and AI may end up helping at some point. So I still hope that formalization will become an important tool for most mathematicians in a not too distant future. We have a lot of work to do in the mean time.

About speed and the blueprint, I think something hasn't been emphasized enough. Every Lean user sometimes wastes a lot of time with stupid technical issues without any mathematical content, even expert users. But my experience is that the true limiting factor is vague mathematical understanding. For me, adding details to the blueprint adds mathematical understanding, or least communicates more mathematical understanding. That the main reason why a very detailed blueprint makes formalization so much faster. It would be nice to give credit to people who take time to write mathematics at a blueprint level of detail (in case they aren't the original authors of the proofs).

When I developed the blueprint infrastructure in 2020, I very much hoped that a blueprint would be an extremely valuable resource for people who want to learn mathematics without caring about Lean. I'm sure the paper on arXiv is great to communicate the PFR proof to experts in additive combinatorics. But I hope that students all over the world will be able to benefit from the blueprint without access to any expert.

About improving the blueprint technology, I first want to comment that the fact that existence of Lean declarations is not checked is a regression coming from the adaptation to Lean 4. The Lean 3 version checked that from the very beginning. When people started to ask for a Lean 4 version and I had no time to do it properly, Utensil (thanks!) quickly hacked a minimal version by modifying about 10 lines of python code, but this was meant as a (very useful) emergency patch, and it threw away some features that required Lean meta-programming. I hope to be able to come back to this around Christmas. Adding more coordination features is definitely possible. However one nice thing with the current setup is that blueprints can be hosted on a fully static website (no code is executed on the server). In particular they can easily be hosted by github.io. One could use more GitHub actions, but it will never bring the flexibility of hosting a website on a server that can actually execute code and access a custom database. I'll try to think about how far we can go with a static website + GitHub actions, but the Mathlib port experience suggests this can become painful pretty quickly.

[llllvvuu]

adding details to the blueprint adds mathematical understanding, or least communicates more mathematical understanding

a blueprint would be an extremely valuable resource for people who want to learn mathematics without caring about Lean

But I hope that students all over the world will be able to benefit from the blueprint without access to any expert.

I can confirm this as a hobbyist. Lean is the first venue I've found to engage with mathematics (however elementary it may be) since college. The potential for education is definitely there.

[Utensil Song]

Patrick Massot said:

About improving the blueprint technology, I first want to comment that the fact that existence of Lean declarations is not checked is a regression coming from the adaptation to Lean 4. The Lean 3 version checked that from the very beginning. When people started to ask for a Lean 4 version and I had no time to do it properly, Utensil (thanks!) quickly hacked a minimal version by modifying about 10 lines of python code, but this was meant as a (very useful) emergency patch, and it threw away some features that required Lean meta-programming. I hope to be able to come back to this around Christmas. Adding more coordination features is definitely possible. However one nice thing with the current setup is that blueprints can be hosted on a fully static website (no code is executed on the server). In particular they can easily be hosted by github.io. One could use more GitHub actions, but it will never bring the flexibility of hosting a website on a server that can actually execute code and access a custom database. I'll try to think about how far we can go with a static website + GitHub actions, but the Mathlib port experience suggests this can become painful pretty quickly.

As @Patrick Massot explained, the emergency patch version of blueprint for Lean 4 came at a cost, it no longer checks the existence of Lean declarations internally. inv check is a rather low-tech solution that makes use of the product of doc-gen4 (which did all the heavy lifting).

Another notable regression from the Lean 3 blueprint is the CI time. Lean 3 blueprint extracts Lean declarations with a short Lean script via meta-programming in a much lightweight way. The logic can't be directly ported to Lean 4 as meta-programming changed significantly since then, but it can be distilled from doc-gen4 which did also much more with these declarations which shoudn't block the build and check of blueprint. So, with Patrick's work, CI time will also be significantly reduced to just a few minutes, the result is that the blueprint will jump to the Github source code like in Lean 3, instead of doc-gen4 which takes longer to build (it seems to hit an optimization bottleneck for now) or it can link to both document and source code, but the document can be async generated.

[Utensil Song]

Also, a short comment on the speed of formalization. As Patrick pointed out, the current model doesn't scale. A significant portion of Lean experts on Mathlib are involved in the project, solved obstacles much more efficiently than the people that other formalization projects might be able to gather, it's more likely a few mathematicians with expertise on the field but only basic Lean expertise, so there will be more technical obstacles to resolve in a much slower speed even with help from experts on Zulip.

Besides that, larger formalization projects will have fundamental issues with formalizing the mathematical constructs in an (almost-)optimal way that wouldn't affect the proving work seriously. Organizing these mathematical constructs in a proper way and in the hierarchies of type class, is a recurring theme for even undergraduate level math, and previous formalization projects (as explained in their formalization papers). It also involves modifying the existing Mathlib in related math branches, which would have to involve more mathematicians and Lean experts for design discussions. Depending on the area of math, this could be the greatest blocking stone.

Lastly, the steps of PFR can be broken down to manageable pieces by almost one mathematician, but this is certainly not the case for a project like FLT and also requires it to scale on the mathematician side. That's where @Kevin Buzzard 's red node idea came from, although the implementation is again only a few lines of Python code, the underlying need is to address the work around "the statement/proof of this result needs to be broken down into smaller formalizable pieces". It will also requires further tooling support for project managements like claiming, status check etc. discussed repeatedly in this topic, which can also be implemented easily with Github Actions, bots, Github Issues, and kanbans in Github Projects.

[Lars Ericson]

Just as LaTeX is now a standard part of the "A-team" mathematician's toolkit, it may come to pass that presenting verified proofs in Lean and using blueprints and various kinds of AI proof assistants will become part of the day to day methodology. As a methodology change, it would help if A-teamers routinely presented a GitHub of Lean code verifying their proofs in their references as evidence of their work, when they publish a proof, i.e., not as an add-on, but as part of the standard of proof of work.

A-listers presenting proof of work in this way, if they verify their own proofs, would need to know Lean to do so. In 1978, nobody know TeX and in 1984 nobody knew LaTeX, but now every A-lister does. Similarly there will be an adoption curve for Lean. This experiment has established that an A-list mathematician can go from Lean newbie to knowing enough to complete state-of-the-art work in the 58 days from October 9th to December 5th.

A methodology change to always verifying proofs would address what some see as a minor reproducibility crisis in mathematics, for example see

• Replication crisis in mathematics
• A Replication Crisis in Mathematics?
• “Reproducible” research in mathematical sciences requires changes in our peer review culture and modernization of our current publication approach

There will probably not be a job category for people who code other people's proofs into Lean. The people doing that now have a passion for symbolic or computational logic or computer science or the topic of verification itself, along with skills and training in the subject matter of mathematics. That is a small community. Whether this community gets funding, and who controls the intellectual property that results, is the topic of articles such as

• Automation compels mathematicians to reflect on our values, Part II
• (In another field, but same problem.) NIH panel calls for fewer, better-paid postdocs in bid to halt loss of scientists to industry

As to the matter of how many authors of lines of code in the PFR proof should be credited explictly by the author of the proof:

• The proof itself, in it's blackboard form, was published prior to it's formal verification.
• So the formal verification is a separate accomplishment.
• It would be reasonable to write up the verification of PFR as a separate article, whose authors, in the tradition of the physics field would be every person that had a hand in it.

As the substance of more and more verified proofs make their way as definitions and theorems into Lean's Mathlib, and into the training of AI proof assistants, it should become easier and easier to verify proofs as a matter of course. In that sense the work of all those Mathlib contributors will become unsung in subsequent verifications that rely on Lean. This is no different from using 20 or 30 different Python packages to get something done, each of which has its own authors and history. That lack of attribution is unavoidable for anybody relying on a large multi-author software product with a long history.