lean-practice

Lean 4 proof snippets and experiments.

# Build the project
lake build

# Type-check specific files in CLI
lake env lean LeanPractice/Obviouslib.lean
lake env lean LeanPractice/Temp0.lean

Learning materials	References
Brief A Tour of Lean Examples Lean 4 tactic cheatsheet (pdf) Game The Natural Number Game Lean Game Server Books Functional Programming in Lean (FPIL) Theorem Proving in Lean (TPIL) Mathematics in Lean (MIL), PDF version Further readings The Hitchhiker's Guide to Logical Verification (pdf) Logic and Proof The Mechanics of Proof Lean 4 VS Code extension manual Metaprogramming in Lean 4, PDF version Lean perfectoid spaces Type Checking in Lean 4 A glimpse of Lean	Docs Lean community The Lean Language Reference A mathlib overview Mathlib documentation Search Loogle, LeanExplore, Moogle, LeanSearch, Lean-Finder LLM-based assist LeanDojo, BFS-Prover-V2, Aristotle other resources REPL, Pantograph, Lean4Web

Learning materials

References

lean-practice is primarily distributed under the terms of the GNU Affero General Public License v3.0 or any later version. See COPYRIGHT for details.