I've got a solid background in software, but I've always had a passion for math. While I shifted to engineering for a practical education, I've recently become interested in COQ and LEAN. I've come across some blogs and videos discussing their usefulness in problem solving. I'm hoping to find a structured roadmap for learning COQ and LEAN, similar to what Exercism offers. My goal is to work on this as a hobby whenever I can carve out some time amidst my busy schedule. I've found that just reading documentation isn't very effective for me, especially with long gaps between study sessions. I'm looking for a curated course pathway that includes interactive exercises and options to recap what I've learned. I should mention that I consider myself pretty average in both math and computers, but I enjoy exploring math-related topics, including algorithms.
1 Answer
I picked up Lean using the book "Functional Programming in Lean." If you've got experience with any ML family language, it should be a bit easier for you to dive into. I found it generally straightforward; however, I did hit a bit of a wall when I started dealing with floating point numbers. Actually getting into proof writing with Lean is quite a challenge though! As for Coq, I tried learning it through "Software Foundations," but it didn’t click for me as well as Lean did. Just give it a shot!
Thanks for the suggestions! I haven’t worked with any ML language yet, but maybe I'll give OCaml a try down the line. I’ll start with the Lean book you mentioned, which I think is accessible on the Lean website. Just a quick question: how long do you think it would take before I could check a proof related to something like a simple Diophantine equation?