Terence TaoI've written a blog post at https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ giving a "quick tour" of the #Lean4 + Blueprint combination used to formalize the proof of the PFR conjecture that I recently completed with Tim Gowers, Ben Green, and Freddie Manners.
Evgenii Zheltonozhskii@tao What environment do you use to write Lean? Have you tried GitHub Copilot or some alternative? Is it helpful?
@evgeniizh this is answered in the post, but in brief; Visual Studio Code; yes; and somewhat.