I've been watching @tao@mathstodon.xyz 's approach to running the Polynomial Freiman-Ruzsa formalisation project with interest. This is Terry's second Lean project; the first was essentially a single-author project, and my understanding is that part of the motivation for embarking on the second was that he wanted to see what a collaborative formalisation experience was like. Having been involved in several of these I would definitely say that they're great fun and that you learn a lot both about cool Lean tricks and about mathematics (e.g. from talking to other humans about the material).

Terry's project will probably be completely done in a week or two, which is of course on the face of it extraordinary -- it is adding more and more weight to the claim that top modern research level combinatorics can now in many cases be formalised in real time. See Bhavik Mehta's post https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/ on my blog for more discussion on the topic of formalising modern combinatorics.

One thing I've learnt from the PFR project is a really powerful use of Patrick Massot's blueprint software: Tao has written LaTeX to break proofs down into bite-sized parts, turning a complex proof into a series of simpler lemmas, proved in LaTeX not Lean, all represented as blue nodes in the blueprint graph https://teorth.github.io/pfr/blueprint/dep_graph_document.html . Every couple of days there are updates from Terry on the Lean Zulip (eg here https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Outstanding.20tasks.2C.20version.203.2E0/near/404022843 ) about who's doing what, and what is up for grabs. Most blue nodes seem to be done in one or just a few Lean sessions, they are nicely-sized projects.

I think these techniques will work very well for a focussed week-long PhD student workshop based on formalising some of the theories needed for the Fermat proof.