HN

Need help?
<- Back
Introduction to Formal Verification with Lean Part 1

Introduction to Formal Verification with Lean Part 1

badcryptobitch

Comments (15)

  • danabramov
    Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4This is the best intro to Lean I know, plus it teaches you why a + b = b + a.
  • rik-x
    (Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
  • raver1975
    I built an automated math research system using Lean to verify the results: https://alethean.org
  • qiqitori
    https://www.amazon.com/Maths-Proofs-Lean-First-Steps-ebook/d... I like this author and a while ago found that he'd published a book on Lean!In the end I wasn't able to read it on my ebook reader and reading it on a PC or smartphone kinda makes it annoying to read on the commute. So I've only read the first two chapters or so but it seemed like a lot of fun. All this talk about using Lean in AI-powered proofs kinda makes me want to pick it up again.
  • dev_dan_2
    Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot).Small feedback: - Great flow, explaination, motivation and so on! :) - Typo: "conext" at the bottom - If you want to keyword-hack a bit, you could introduce a paragraph or too about the role the relationship of Lean4 with LLMs/AI ;)
  • charlieyu1
    I just wish Lean4 is easier to use. Tried Mathematics in Lean and couldn’t even get the dependencies right
  • smasher164
    a) Thanks for putting this together!b) Please don't hijack my scrolling.c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.
  • SnehRJoshi
    [flagged]