Post #1366381

2023-11-27 09:29 UTC

@andrejbauer @tao Only combinatorics. I still maintain that it would be an extremely long project to even *state* the main theorems in any of the recent papers written by Toby Gee or Ana Caraiani, two other number theorists in my department. And proving them would be completely inaccessible -- even proving FLT is a gigantic project and this is from the 90s. There are still lots of problems in the way of making formalisation of all modern mathematics easy.

Replies (1)

@tao@mathstodon.xyz 2023-11-27 16:20

@xenaproject @andrejbauer One thing this project has made me realize is that the mathematical side of the project - as encapsulated by writing and maintaining the Blueprint (as well as docstrings and comments) - is as important as the formalization side. The PFR project is short enough and elementary enough that I was able to write a blueprint (cribbed in large extent from the actual paper) in advance of most of the Lean formalization, but for a larger project the two would proceed in parallel, and one would need a significant group of people to develop the blueprint. However, the set of skills required for that is somewhat different - one can recruit mathematicians who are familiar with the content but have only minimal experience in Lean to work on tasks on the blueprint (similar to how PFR is distributing tasks for formalization), operating with only loose coordination with the formalization group who need competence in Lean but only minimal experience with the mathematics., For a large project there should also be a mostly separate administrator/moderator group that deals with coordination, structure, and the "big picture" rather than atomized formalization or documentation. (One can in principle work on more than side, but I found this to not be the optimal use of my time, also I tended to abuse the administrator privilege of pushing code without passing CI checks.) With PFR I have started getting a few pull requests on the blueprint / docstring side of things that have also been valuable; but one key difference is that they require much more human review, in contrast with say filling in a Lean sorry for which one can largely outsource the review to the CI checks.

Open ##1471880