Formalizing the proof of PFR in Lean4 using Blueprint

Posted on by

This in my feed today: Formalizing the proof of PFR in Lean4 using Blueprint: a short tour by Terence Tao. I would like to learn Lean.

Leave a Reply