|
|
|
|
|
by rramadass
6 days ago
|
|
Assuming you are serious; there is a lot to know conceptually before one can answer the above comprehensively. Start with Set Theory, Propositional/Predicate Calculus, Hoare Triples, Dijkstra's wp-calculus and Predicate Transformers, then move on to Lambda Calculus, Type Systems (inductive/dependent/function etc.), Curry-Howard Correspondence, Invariants/Verification Conditions/Theorems etc. all leading up to "How the hell do they all come together in a Theorem Prover?" Some simple tutorials; Introduction to Lean for Programmers: The syntax and semantics of mathematics - https://towardsdatascience.com/introduction-to-lean-for-prog... The hitchhiker's guide to reading Lean 4 theorems - https://blog.lambdaclass.com/the-hitchhikers-guide-to-readin... |
|