First Project with Lean and Mathlib

Generated by lean-docgen.

• Project and Dependency Documentation

Links

• Functional Programming in Lean @ 4.1.0
  • Newer version @ 4.21.0
• Theorem Proving in Lean
• Mathematics in Lean
• Metaprogramming in Lean
  • Short introduction
• How to Prove It - with Lean
• Hitchhiker’s Guide to Logical Verification
• Glimpse of Lean
• The Mechanics of Proof

See also

• Next steps from FPIL
• Community sources for learning Lean 4
• Significant changes in Lean 4 from Lean 3
• Batteries (previously std4)
• Typechecking in Lean 4
• Foundations of Lean
• The HoTT Book
• Rocq : mathematical components
• Software Foundations @ UPenn
• Type driven development with Idris