About Lean 4 Dev
Lean 4 Dev is an independent learning site for people who want to understand Lean 4 as both a programming language and an interactive theorem prover.
What this site publishes
The site focuses on practical, beginner-friendly explanations of Lean 4 syntax, functional programming, tactics, proof workflows, Mathlib, and project tooling. The goal is to help readers move from reading examples to running Lean code in their own editor.
Lean 4 Dev is not an official Lean project and is not affiliated with the Lean Focused Research Organization. Official resources are linked where they are the right next step for deeper reference.
Editorial responsibility
Content is published by the Lean 4 Dev Editorial Team. Lessons are written for learners, checked for clarity, and reviewed against runnable Lean examples whenever code appears in a guide.
See the editorial policy for how guides are researched, corrected, and updated.
What readers can expect
- Original explanations written for learners, not copied reference text.
- Runnable Lean snippets that show the idea being taught.
- Clear separation between programming lessons and theorem proving lessons.
- Links to official Lean, Mathlib, and community resources when useful.
Contact
Questions, corrections, and feedback are welcome through the contact page: lean4.dev/contact.