Zulip Chat Archive

Stream: new members

Topic: Getting started ?


view this post on Zulip Fox Juan (Mar 20 2019 at 19:47):

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 ?

view this post on Zulip Patrick Massot (Mar 20 2019 at 19:54):

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

view this post on Zulip Patrick Massot (Mar 20 2019 at 19:54):

It's only mention in the introduction

view this post on Zulip Kevin Buzzard (Mar 20 2019 at 20:00):

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.

view this post on Zulip Kevin Buzzard (Mar 20 2019 at 20:01):

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

view this post on Zulip Kevin Buzzard (Mar 20 2019 at 20:05):

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


Last updated: May 14 2021 at 14:20 UTC