3 ms·
Which tutorial did you use? As someone coming from computer science, I found https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/
by foooobar 7y ago
Which tutorial did you use?
As someone coming from computer science, I found https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/ very approachable as an introduction to ITP in general.
- mherrmann 7y agoThat's the one I meant I think. It is nice, but as I said the impression it left me with was "you could have told me how the approach generally works sooner".
- lonelappde 7y agoThat books wants to build the foundation (dependent types) before making the big claim in chapter 3. It's a bit weird because has Haskell shows, you don't need dependent types for basic theorem proving. (but dependent types do give a lot of useful power)
- dwohnitmok 7y agoWell if you just have Haskell 2010 types, you're talking about really really basic theorem proving since all you have is propositional logic. The most interesting thing I can think of to prove with Haskell 2010 types is (the constructive version of) de Morgan's laws. Almost all other interesting mathematical statements are out of reach.