Why?

If Dwarf Fortress is the most complex simulation ever built and Factorio is crystallized obsession in game form, then Lean is what happens when you point that same energy at the foundations of mathematics. You write code to solve puzzles, and the compiler gives you immediate feedback on whether you succeeded. Like Dwarf Fortress, losing is fun, because even a failed proof attempt teaches you something about why it failed. Like Factorio, there is always one more lemma to optimize, one more proof to refactor, one more elegant solution lurking just beyond the current mess.

Maybe you want to understand how markets actually work, not the hand-wavy version but the mathematical objects underneath. Maybe you want to learn what the engineers at top quant firms and AI labs are learning, because that seems like a reasonable bet on where things are heading. Maybe you are interested in programming languages, or how computers can check human reasoning. Maybe you have no practical reason at all and just want to learn something new. All of these are good reasons.

Lean sits at the intersection of programming and mathematics. You can use it to write programs that the compiler verifies are correct. You can use it to prove mathematical theorems and have a machine check your work, like your 8th grade algebra teacher but less forgiving. You can use it to explore ideas about types, logic, and computation that simply cannot be expressed in mainstream languages. Or you can just mess around and see what happens. There is no entrance exam.

There are also practical reasons. The world runs on systems that allocate resources: power grids balancing supply and demand, networks routing packets, markets matching buyers and sellers. These systems are mathematical objects, and their correctness matters. A bug in market infrastructure does not just crash a server; it misallocates capital, distorts prices, rewards the wrong participants. Formal methods let you prove properties about such systems before deployment. The matching algorithm that assigns medical residents to hospitals, the slot allocation system that schedules aircraft landings across congested airspace, high-assurance trading systems: these are theorems waiting to be verified. The gap between “we tested it extensively” and “we proved it correct” is the gap between confidence and certainty. For systems where the stakes justify the effort, that gap matters.

The honest truth is that most people do not need dependent type theory or formal verification for their day jobs. But necessity is a boring criterion for what to learn. People study ancient languages, play chess, learn to cook elaborate dishes, prove that there are infinitely many primes. The question is not whether you need something but whether it interests you.

If you are curious about what it means to prove something with absolute certainty, Lean can show you. When a proof type-checks, it is correct. Not “probably correct” or “correct assuming the tests pass” but mathematically, definitively correct. The compiler does not care about your reputation or your confidence. It cares whether the logic holds. There is something clarifying about that. You discover what you actually understand versus what you thought you understood. A proof assistant is a bicycle for the mind: it does not think for you, but it amplifies your ability to think correctly (and increasingly, to constrain the output of language models).

Lean is also difficult. It will not let you wave your hands. It will not accept “it is obvious that”, “because of abstract nonsense” or “this margin is too narrow to contain the proof” as justifications. The feedback loop is immediate and unforgiving. This can be frustrating, but it is also what makes the successes satisfying. When a proof finally compiles, you know it works.

There is a kind of peace in this. The world outside is uncertain, full of claims that cannot be verified, arguments that cannot be resolved, systems that fail in ways no one predicted. Inside a proof assistant, the rules are clear. A theorem holds or it does not. The machine tells you which. You can build something that will still be correct in a hundred years, long after the context that motivated it has faded. This is craftsmanship: making things that work, that endure, that do not depend on luck or circumstance. The difficulty is part of the appeal. Easy things do not teach you much, and they do not last.

If this sounds interesting, keep reading. If not, there are plenty of other things worth learning.

Why Lean Specifically?

Among proof assistants, several mature options exist: Coq, Agda, Isabelle, and others each have devoted communities and decades of development. Lean 4 occupies a distinctive position among them. It is simultaneously a theorem prover backed by a million-line mathematical library and a general-purpose programming language fast enough for production use. You can prove theorems about prime numbers in the morning and write a web server in the afternoon, using the same language, the same tools, the same mental model.

The system emerged from Microsoft Research in 2013 and has evolved through four major versions. Lean 4, released in 2021, was a ground-up rewrite that reimagined the tool as both proof assistant and practical programming language. The implementation is largely written in Lean itself, a feat of bootstrapping that demonstrates the language’s capabilities. The mathematical library, Mathlib, contains over a million lines of formalized mathematics spanning algebra, analysis, topology, number theory, and beyond.

Lean has better tooling than other theorem provers. The error messages are informative. The IDE integration works. You can ask for hints, search the library, and see exactly what remains to prove. The more you practice, the better you get, and the more you learn about the deep structure of mathematics itself.

This article series is my (admittedly flawed) attempt to take you from zero knowledge of Lean to writing your own proofs and programs, with enough depth to tackle real problems. Whether you finish it or abandon it halfway through, whether you master the material or merely glimpse its outlines, you will have spent your time on something worthwhile. In a world of endless distractions optimized to capture attention without rewarding it, maybe that counts for something.