A course for a very newbie

Stream: general

[Byung-Hak Hwang]

Hello, I'm new to Lean and recently read an article on Terence Tao's blog about formalizing the PFR conjecture, which sparked my interest in this area. I completed the Natural Number Game designed by Kevin Buzzard and read some articles about what Lean is.

Now, I’m planning to formalize my mathematical work in combinatorics and representation theory. Given that I have only a little knowledge of Lean, what should I do first to ensure the success of my project? Additionally, I’m interested in using the blueprint tool developed by Patrick Massot.

Any guidance on how to proceed would be greatly appreciated!

[Daniel Weber]

Maybe this should be moved to #new members . Anyway, there's a list of resources in https://leanprover-community.github.io/learn.html , you could read one of the books there. There are also a few more games on https://adam.math.hhu.de/#/ . Other than that, I'd recommend just diving into it, and asking here if you're unsure how to do something

[Kevin Buzzard]

Start by writing some LaTeX explanation of a proof in a blueprint framework, and then assign some Lean names to each theorem and definition and then make a little blueprint graph and then start filling in proofs.

[Byung-Hak Hwang]

Daniel Weber 말함:

Maybe this should be moved to #new members . Anyway, there's a list of resources in https://leanprover-community.github.io/learn.html , you could read one of the books there. There are also a few more games on https://adam.math.hhu.de/#/ . Other than that, I'd recommend just diving into it, and asking here if you're unsure how to do something

Oh, I didn't know #new members . Thank you for your advices. I'll try to just dive into the project!

[Byung-Hak Hwang]

Kevin Buzzard 말함:

Start by writing some LaTeX explanation of a proof in a blueprint framework, and then assign some Lean names to each theorem and definition and then make a little blueprint graph and then start filling in proofs.

Thank you so much! I'll follow your guide :)