Blog post "tour" of project

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

I wrote a blog post giving a "quick tour" of the PFR project at

https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/

Comments welcome.