A collection of formal mathematics proofs written in Lean 4, using the Mathlib4 library. This repository covers foundational theorems across multiple areas of mathematics, with a focus on building rigorous, machine-verified proofs.
git clone https://github.com/Dean-Foulds/lean_projects
cd lean_projects
lake exe cache get # Download precompiled Mathlib (saves hours of build time)
lake buildlean_projects/
├── LeanProjects/
│ ├── analysis_basics.lean # Real analysis & calculus
│ ├── combinatorics_basics.lean # Combinatorics & finite sets
│ ├── decide_theorems.lean # Decidability theorems
│ ├── fifth_lookup.lean # Lookup & search theorems
│ ├── hello.lean # Introduction to Lean 4
│ ├── linear_algebra_basics.lean # Vector spaces & linear maps
│ ├── logic_basics.lean # Logic & type theory
│ ├── playground.lean # Experimental proofs
│ ├── rfl_theorems.lean # Reflexivity theorems
│ └── squeeze.lean # Squeeze theorem & inequalities
├── lakefile.toml # Lake build configuration
├── lean-toolchain # Lean version pinning
└── README.md
- Absolute value non-negativity
- Triangle inequality
- Square non-negativity
- Positivity implications
- Modus ponens
- Double negation elimination
- De Morgan's laws
- Conjunction commutativity
- Sum of first n natural numbers
- Finite set cardinality
- Empty set properties
- Vector addition commutativity
- Scalar multiplication distributivity
- Zero vector identity
- Lean 4 — Functional programming language & theorem prover
- Mathlib4 — Community mathematics library
- Lake — Lean build system
Dean Foulds — Data Scientist & ML Engineer
🌐 deanfoulds.xyz | 💼 LinkedIn | 🐙 GitHub
MIT