Lean 4 101 for Python Programmers: A Gentle Introduction to Theorem Proving

Before we begin — if you're interested in improving engineering quality and developer workflows, check out git-lrc on GitHub — a free micro AI code review tool that runs on every commit. If the idea resonates with you, consider giving the project a ⭐ on GitHub.

Python developers are used to expressive code.

You can automate workflows in minutes, prototype products quickly, manipulate huge datasets, and build entire backends with surprisingly little code.

But eventually many developers run into a frustrating problem:

“How do I know my program is actually correct?”

You can write tests.
You can add type hints.
You can run linters.

But tests only sample behavior.

They do not prove correctness.

That’s where Lean becomes fascinating.

Lean 4 is not just a programming language.

It’s also:

• a theorem prover
• a proof assistant
• a functional programming language
• and a system for mathematically verifying software

If you’re coming from Python, Lean can feel strange at first.

But once the mental model starts clicking, it genuinely changes how you think about programming.

This article is a beginner-friendly introduction to Lean 4 specifically for Python programmers.

The Biggest Difference: Lean Wants Precision

Python is flexible by design.

For example:

def add(a, b):
    return a + b

Python is happy with this.

But think carefully:

• What types are a and b?
• Integers?
• Strings?
• Lists?
• Custom objects?

Python delays those decisions until runtime.

Lean does the opposite.

In Lean:

def add (a : Nat) (b : Nat) : Nat :=
  a + b

This explicitly says:

• a is a natural number
• b is a natural number
• result is a natural number

At first this can feel verbose to Python developers.

But Lean’s philosophy is interesting:

Ambiguity is usually hidden complexity.

Lean tries to eliminate hidden assumptions.

Your First Lean Functions

Let’s compare Python and Lean side by side.

Python:

def square(x):
    return x * x

Lean:

def square (x : Int) : Int :=
  x * x

Very similar.

Now let’s try something slightly more interesting.

Python factorial:

def factorial(n):
    if n == 0:
        return 1
    return n * factorial(n - 1)

Lean factorial:

def factorial : Nat → Nat
| 0 => 1
| n + 1 => (n + 1) * factorial n

This looks unusual initially.

What’s happening here?

Lean uses pattern matching.

Explanation:

• if input is 0, return 1
• otherwise treat the number as n + 1
• recursively compute factorial

This style is extremely common in functional programming.

And importantly:

Lean can reason formally about recursive definitions.

Lean Cares Deeply About Correctness

Here’s a subtle Python issue:

def divide(a, b):
    return a / b

Looks harmless.

But:

divide(10, 0)

Runtime error.

Python lets dangerous states exist until execution.

Lean pushes you to think earlier.

For example, Lean separates different numeric systems carefully:

• natural numbers
• integers
• rational numbers
• finite values

That strictness is not accidental.

Lean assumes:

if something matters logically, it should be represented explicitly.

This is one reason theorem provers are powerful.

Immutable Thinking Feels Different

Python programmers often mutate state:

count = 0

def increment():
    global count
    count += 1

Lean strongly prefers immutable transformations:

def increment (n : Nat) : Nat :=
  n + 1

Instead of changing existing state:

• input goes in
• new value comes out

Why is this important?

Because mutable state becomes difficult to reason about formally.

Imagine trying to mathematically prove correctness of a large system where:

• variables change everywhere
• functions have hidden side effects
• execution order matters constantly

Functional programming reduces this chaos.

That’s one reason languages like Lean heavily embrace immutability.

Types in Lean Are Much More Powerful Than Python Type Hints

Python type hints help developers.

Lean types help prove things.

That’s a huge distinction.

Python:

def greet(name: str) -> str:
    return "Hello " + name

Helpful, but not enforced rigorously.

Lean types can encode logical guarantees.

For example, you can express:

• “this list cannot be empty”
• “this number is positive”
• “this function always terminates”

That’s where Lean starts feeling less like programming and more like formal reasoning.

A tiny theorem:

theorem add_zero (n : Nat) : n + 0 = n := by
  rfl

This proves:

adding zero changes nothing

Breaking it down:

• theorem declares a proposition
• (n : Nat) means for any natural number n
• : n + 0 = n is the claim
• by starts proof mode
• rfl means “this is true by direct simplification”

This may look trivial.

But Lean scales this exact mechanism to verify extremely sophisticated systems.

Lean Proofs Feel Like Interactive Debugging

One surprising thing about Lean:

Writing proofs often feels similar to debugging.

Suppose we define list length.

def length : List α → Nat
| [] => 0
| _ :: xs => 1 + length xs

Explanation:

• empty list has length 0

• otherwise:

  • ignore first element (_)
  • recursively compute remaining length

Now imagine proving something about lists.

Lean gives continuous feedback:

• current assumptions
• proof goals
• missing logical steps

This creates a very interactive workflow.

Python developers often enjoy REPL-driven development.

Lean has a similar “conversation with the system” feeling.

Except instead of debugging runtime behavior, you debug logical reasoning.

Tactics: Step-by-Step Proof Construction

Lean proofs are often built using tactics.

Example:

theorem reverse_reverse (xs : List Nat) :
  xs.reverse.reverse = xs := by
  simp

What does this mean?

It proves:

reversing a list twice returns the original list

And simp tells Lean:

simplify using known rules

Some useful beginner tactics:

• simp → simplify expressions
• rw → rewrite using known equalities
• intro → introduce assumptions
• exact → directly provide proof
• apply → use another theorem

Think of tactics like:

• debugging tools
• proof-building commands
• interactive reasoning helpers

Over time they become surprisingly intuitive.

Lean Quietly Improves Your Software Engineering

Even if you never become a theorem proving expert, Lean changes how you think.

You start asking:

• What assumptions exist here?
• What invariants should always hold?
• Can invalid states exist?
• Is this behavior guaranteed?

This mindset transfers back into ordinary engineering.

You often begin writing:

• cleaner APIs
• safer abstractions
• more predictable systems
• more explicit contracts

Ironically, learning Lean can improve your Python.

How Python Developers Should Learn Lean

A good beginner path:

1. Learn basic functional programming ideas

Focus on:

• recursion
• immutability
• pattern matching

2. Install Lean + VS Code

Using Visual Studio Code with the Lean extension gives excellent feedback.

3. Ignore advanced math initially

Many beginners get overwhelmed because online discussions quickly become abstract.

Start simple:

• functions
• lists
• recursion
• tiny proofs

4. Build tiny programs

Good practice ideas:

• reverse a list
• binary trees
• arithmetic functions
• list transformations

5. Expect gradual progress

Lean is closer to learning chess or mathematics than learning a typical framework.

The intuition develops slowly.

Conclusion

Lean 4 represents a very different philosophy of programming.

Python asks:

“Can we make development faster and more flexible?”

Lean asks:

“Can we make reasoning precise and verifiable?”

Both philosophies matter.

But as software systems become increasingly complex — especially in:

• AI
• infrastructure
• cryptography
• finance
• distributed systems

— the ability to formally reason about correctness may become far more important.

And perhaps that’s the most interesting thing about Lean:

It doesn’t just teach syntax.

It teaches disciplined thinking.

So here’s a question to leave you with:

If AI increasingly generates code automatically, do developers become more valuable not for writing code — but for verifying whether systems are actually correct?

That future may arrive sooner than we think.

And if it does, theorem provers like Lean may eventually move from research circles into mainstream software engineering.

And again — if you're interested in developer tooling around engineering quality, check out git-lrc on GitHub — a free micro AI code review tool that runs on commits — and consider giving the project a ⭐ if you'd like to support it.