🔮 Lean 4 toolkit

this repository contains examples and explanations as i learn Lean 4 (a powerful theorem prover and programming language for the AI age)

---

installation

on macos

curl -L https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-apple-darwin.tar.gz | tar xz
./elan-init
source $HOME/.elan/env

on linux

curl -L https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init
source $HOME/.elan/env

test the installation with:

lean --version
lake --version

---

running

project structure

• src.lean: the main entry point for the source code
• src/: source code for concepts and examples/
• lakefile.lean: the lean package manager configuration file
• lean-toolchain: specifies the Lean version for the project (elan manages the compiler toolchains)
• Makefile: specify all available commands

make build

run all src/*.lean files with:

make build

basic types, theorems, type classes...

run any other file inside src/example/ following its command inside Makefile.

---

study resources

my notes

• basics
• formal verification
• advanced concepts

learning lean and theorem proving

• ✅ learn Lean from lean-lang.org
• ✅ Lean prover community
• 🟡 Lean 4 documentation
• 🟡 mathematics in Lean
• 🟡 learning mathematics with lean (videos)
• 🟡 theorem proving in Lean 4
• 🟡 the matrix cookbook with code
• 🟡 the Lean 4 theorem prover and programming language
• 🟡 more theorem proving in Lean 4
• 🟡 an extensible theorem proving frontend
• 🟡 a metaprogramming framework for formal verification
• 🟡 terence tao on future of AI in mathematics
• 🟡 the mechanics of proof
• 🟡 partial Lean formalization of analysis I
• 🟡 welcome to the natural number game

useful

• vscode/cursor plugin
• mathlib algebra methods ref
• zulip Lean channel
• moogle.ai (find theorems)

applied examples

• Lean prover community's blog and projects
• social choice theory in Lean (code)
• the deep link equating math proofs and computer programs
  • "types are fundamentally equivalent to logical propositions"
• AI safety via debate, by g. irving et al (2018)
  • "in the debate game, it is harder to lie than to refute a lie"
• meta's teaching AI advanced mathematical reasoning
  • *"our method, HyperTree Proof Search (HTPS), is trained on a dataset of successful mathematical proofs and then learns to generalize to new, very different kinds of problems. It was able to deduce a correct proof for an IMO problem that involved some arithmetic reduction to a finite number of cases"