Shamrock-Frost/lean4

Lean 4 programming language and theorem prover

This is the repository for Lean 4.

We provide nightly releases and have just begun regular stable point releases.

About

• Quickstart
• Walkthrough installation video
• Quick tour video
• Homepage
• Theorem Proving Tutorial
• Functional Programming in Lean
• Manual
• Release notes starting at v4.0.0-m3
• Examples
• External Contribution Guidelines
• FAQ

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.