Getting started ?

Stream: new members

[Fox Juan]

What is the prerequisites for LEAN ? I have started reading the introduction over leanprover.github.io and hit a wall at "Resolution theorem provers", quickly looked up the page on Wikipedia but couldn't understand the formulas. I'm a quit good programmer, but looks like my primitive high school math won't allow me to understand the source code of this language. What sources could you recommend to get up to speed ?

[Patrick Massot]

You don't need to know what "resolution theorem prover" means to read that book

[Patrick Massot]

It's only mention in the introduction

[Kevin Buzzard]

By "understand the source code of this language" do you mean "read the C++ code to see how Lean works?" or "understand Lean code"? I have no idea what the C++ code is doing (how Lean works) but I have written a bunch of Lean code.

http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html

is some beginner stuff, you don't need any maths for that.

[Kevin Buzzard]

/me still hasn't written the beginner book which he so desperately wants to write...

[Kevin Buzzard]

https://xenaproject.wordpress.com/2017/10/31/building-the-non-negative-integers-from-scratch/ also seems to go down well with mathematicians