Lean-4-Literature

Beginner friendly

1. Theorem Proving in Lean 4 - Use Lean 4 as a proof assistant to prove theorems.
2. Functional Programming in Lean - Use Lean 4 as a programming language.
3. Mathematics in Lean - Use Lean 4 to do 'common' mathematics.
4. The Mechanics of Proof - Use Lean 4 to do 'common' mathematics.
5. The Hitchhiker's Guide to Logical Verification - Use Lean 4 to do 'common' computer science.
6. Logic and Proof - Use Lean 4 to do logic in Lean 4.

Intermediate and onwards

1. Metaprogramming in Lean 4 - Extend Lean 4 with custom functionality.
2. Type Checking in Lean 4 - Learn about Lean 4 metatheory.
3. Scientific Computing in Lean - WIP - Modern approach to scientific computing melding convenience of use, correctness, and performance.
4. The Lean Language Reference - The language reference.

This list is a superset of documentation recommended at the official Lean 4 website.

Lean-4-not-so-Literature

WARNING: subjective and broad; grain of salt recommended, reader discretion required.

List of thoughts/guidelines. While I may use examples to explain what to do / not to do - I do not say why for the sake of brevity. Why left as an exercise for the reader. While I am happy to discuss nuances and pertinence of these at length, this is not a repo in which to do it.

Environment

1. Use VS Code and its Lean 4 extension.
2. Use JuliaMono font.

Lean

1. Do not (ab)use dependent types. Give strong preference to extrinsic properties.

section Bad
def foo (n : Nat) : { m : Nat // 42 < m } := ...
end Bad

section Good
def foo (n : Nat) : Nat := ...
theorem 42_lt_foo {n : Nat) : 42 < foo n := ...
end Good

2. Do not unfold more than 1 definition per theorem. State lemmas about definitions you use, unfold these definitions in the lemmas that are specifically about them.

3. Only use simp [...] (and its derivatives, a'la aesop) to discharge the enclosing goal - i.e. as the final tactic in a goal. Use simp only otherwise. Invoking simp? gives you the appropriate simp only to use, if you 'must' use simp in the middle of a proof.

A part of my job is to address Lean-specific issues - I use this repository for my own reference, but I am happy to accept PRs. If they gucci.