Formalizing the proof of PFR in Lean4 using Blueprint: a short tour

I find it almost scary how casual Terry is about all this. Comparing this to my own humble attempts at graduate math, I feel like a caveman trying to rock a basic wheelbarrow who just gets a visit from a guy in a helicopter. And then that guy is stretching out his hand &#x27;Here, try it out, it&#x27;s fun, useful and not scary at all&#x27;.<p>It was always clear to me that formalization was the future of math ever since I heard about the four-color theorem. What I did not anticipate, and what Terry seems to take in stride here, was that we&#x27;d get an AI that can <i>almost</i> do the job of writing the math as well around the same time as formalization starts to gain traction. The fact that I get to learn about it from the most friendly and humble generational genius is just the cherry on top.

In the last comment below he writes<p>&gt; The project has now completed its primary goals; the entire dependency graph is now green.

Ok, I&#x27;ll download lean4 and read the tutorials. Everything else I&#x27;ve tried that Prof. Tao has suggested has worked well. I didn&#x27;t really realize that proof software had advanced so far. I tried to do a project in undergrad to put a lot of ZFC into Prolog but it was just too early to work.

I don&#x27;t follow how the proof text is generated from lean? Or is it not, they are doing the verification in lean and the proof text is completely separate.<p>Looking at the project more I see it&#x27;s the latter. Turning lean tactics into readable proof text would be hard, as the lean phrase book he is keeping shows: <a href="https:&#x2F;&#x2F;docs.google.com&#x2F;spreadsheets&#x2F;d&#x2F;1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo&#x2F;edit#gid=0" rel="nofollow noreferrer">https:&#x2F;&#x2F;docs.google.com&#x2F;spreadsheets&#x2F;d&#x2F;1Gsn5al4hlpNc_xKoXdU6...</a>

I find his comment on Copilot to be enlightening. He says it’s not always right, but he still finds it useful. Kinda like that old saying in stats “all models are wrong, but some models are useful”. Language models are really helpful when you have enough experience to be able to judge when it fails, I do feel sorry for novices who don’t have enough experience yet to do that.

Lean has been a really exciting thing for me to watch (as an amateur observer), it&#x27;s gonna go right up to the limits that Godel found.