search

avigad / lamr

Logic and Mechanized Reasoning
82 stars 20 forks source link

Is there an appropriate place to ask questions about the book? #8

Closed dabrahams closed 4 weeks ago

dabrahams commented 4 weeks ago

For example, the exercises in the chapter on using Lean as an FP language contain a couple of "Prove in Lean that…” questions, that seem to require knowledge the book would have contained since it's walking me through the much simpler fundamentals of using Lean to write programs. I don't know how to approach these exercises. Should I work through the very substantial tutorial on Lean theorem proving first? It seems like opening issues here must be the wrong vehicle for questions like this one…

avigad commented 4 weeks ago

Most of the book uses Lean as a programming language to implement logic-based algorithms or to connect with SAT- and SMT-solvers. Nothing bad will happen if you ignore the parts that ask you to think about Lean as a proof assistant. But if you do want to learn more about Lean as a proof assistant, I recommend looking at Mathematics in Lean, exploring the Lean Community web pages, and checking out the Lean Zulip social media channel.

dabrahams commented 4 weeks ago

Thanks for your advice.

I recommend looking at Mathematics in Lean,

That's a better place to start than the tutorial I linked?

avigad commented 4 weeks ago

The introduction to MIL explains the difference in approach. TPIL explains the system and its foundations from the bottom up, while MIL is designed to get you proving theorems as quickly as possible. For verifying programs, the Hitchhiker's Guide to Formal Verification in Lean is better. You can find a guide to learning resources here.

dabrahams commented 4 weeks ago

many thanks!