DEV Community

Shrijith Venkatramana
Shrijith Venkatramana

Posted on

Lean 4 for Programmers: Building a Todo List with Proof

#ai #productivity #programming #webdev

Hello, I'm Shrijith Venkatramana. I'm building git-lrc, an AI code reviewer that runs on every commit. Star Us to help devs discover the project. Do give it a try and share your feedback for improving the product.

Most programmers already write specifications.

They just don't call them that.

Whenever you write:

assert user.id is not None
Enter fullscreen mode Exit fullscreen mode

or:

if (!task.completedAt) throw Error(...)
Enter fullscreen mode Exit fullscreen mode

you are encoding invariants informally.

The problem is:
the compiler does not know them.

So your system eventually drifts into illegal states.

That is where Lean 4 becomes interesting.

Lean is not merely a theorem prover. It is a programming language where:

  • types can encode invariants,
  • proofs are first-class objects,
  • illegal states can become unrepresentable.

In this article, we will build a tiny todo system in Lean 4 and prove some properties about it.

Not because todo apps matter.

But because mundane software hides surprisingly rich semantics.

Installing Lean 4

The easiest path is:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Enter fullscreen mode Exit fullscreen mode

Then:

lake new todo-proof
cd todo-proof
Enter fullscreen mode Exit fullscreen mode

Open it in VSCode with the Lean extension.

Your First Lean Program

Let's start with a simple structure.

structure Task where
  id : Nat
  title : String
  completed : Bool
deriving Repr
Enter fullscreen mode Exit fullscreen mode

This is similar to:

@dataclass
class Task:
    id: int
    title: "str"
    completed: bool
Enter fullscreen mode Exit fullscreen mode

Now create a value:

def task1 : Task :=
  { id := 1
    title := "Learn Lean"
    completed := false }
Enter fullscreen mode Exit fullscreen mode

And evaluate it:

#eval task1.title
Enter fullscreen mode Exit fullscreen mode

Functions are Pure

Let's write a function to complete a task.

def completeTask (t : Task) : Task :=
  { t with completed := true }
Enter fullscreen mode Exit fullscreen mode

Test it:

#eval (completeTask task1).completed
Enter fullscreen mode Exit fullscreen mode

Unlike mutable application code, Lean encourages modeling transitions explicitly.

That becomes important once proofs enter the picture.

Lists of Tasks

Now define a todo list.

abbrev TodoList := List Task
Enter fullscreen mode Exit fullscreen mode

Add tasks:

def addTask (todos : TodoList) (task : Task) : TodoList :=
  task :: todos
Enter fullscreen mode Exit fullscreen mode

Example:

def todos :=
  addTask [] task1
Enter fullscreen mode Exit fullscreen mode

The First Invariant

Real systems care about invariants.

Suppose:

No two tasks should share the same ID.

In JavaScript this is convention.

In Lean we can state it formally.

Extracting IDs 

def ids (todos : TodoList) : List Nat :=
  todos.map (fun t => t.id)
Enter fullscreen mode Exit fullscreen mode

Unique IDs Predicate

Lean already has List.Nodup.

It means:

this list contains no duplicates.

Now define:

def UniqueIds (todos : TodoList) : Prop :=
  List.Nodup (ids todos)
Enter fullscreen mode Exit fullscreen mode

This is our first specification.

Notice something subtle:

Prop
Enter fullscreen mode Exit fullscreen mode

means:

a logical proposition.

Not a runtime boolean.

Proving Something

Let's prove:

an empty todo list has unique IDs.

theorem empty_has_unique_ids :
  UniqueIds [] := by
  unfold UniqueIds ids
  simp
Enter fullscreen mode Exit fullscreen mode

That tiny proof already demonstrates the core idea.

We encoded:

  • a system property,
  • mathematically,
  • and mechanically verified it.

Safe Task Addition

Now we define safer insertion.

We only allow adding a task if its ID is fresh.

First:

def idExists (todos : TodoList) (id : Nat) : Bool :=
  todos.any (fun t => t.id == id)
Enter fullscreen mode Exit fullscreen mode

Then:

def addTaskSafe (todos : TodoList) (task : Task) : Option TodoList :=
  if idExists todos task.id then
    none
  else
    some (task :: todos)
Enter fullscreen mode Exit fullscreen mode

This resembles production code more closely.

Proving Correctness of Safe Addition

Now the interesting part.

We want:

If the original list had unique IDs,
and insertion succeeds,
the resulting list also has unique IDs.

In theorem-prover land, this is the real API contract.

A simplified proof sketch:

theorem addTaskSafe_preserves_unique
    (todos : TodoList)
    (task : Task)
    (h : UniqueIds todos)
    (hadd : addTaskSafe todos task = some (task :: todos)) :
    UniqueIds (task :: todos) := by
  unfold addTaskSafe at hadd
  unfold UniqueIds at *
  simp at hadd
  aesop
Enter fullscreen mode Exit fullscreen mode

Do not worry if this feels strange initially.

The important conceptual shift is:

We are proving:

  • state transitions preserve invariants.

That is the heart of formal methods.

Illegal States

Most application bugs reduce to:

invalid transitions between states.

For example:

{
  completed: true,
  completedAt: null
}
Enter fullscreen mode Exit fullscreen mode

This is an illegal state.

Traditional systems allow it accidentally.

Lean encourages modeling state explicitly.

Encoding State in Types

Instead of:

structure Task where
  completed : Bool
Enter fullscreen mode Exit fullscreen mode

we can do:

inductive Status where
  | active
  | completed
Enter fullscreen mode Exit fullscreen mode

Now:

structure Task where
  id : Nat
  title : String
  status : Status
Enter fullscreen mode Exit fullscreen mode

Already better.

But we can go further.

Dependent Thinking

Suppose completed tasks must contain a completion timestamp.

In mainstream languages:

completedAt?: Date
Enter fullscreen mode Exit fullscreen mode

In Lean:

inductive TaskState where
  | active
  | completed (finishedAt : Nat)
Enter fullscreen mode Exit fullscreen mode

Now the timestamp exists iff the task is completed.

The illegal state disappears entirely.

This is a recurring pattern in theorem proving:
move runtime checks into type structure.

Why This Matters

At first glance, this seems academic.

But think about real systems:

  • payment processors,
  • distributed databases,
  • auth systems,
  • CI pipelines,
  • infrastructure tooling.

Most failures come from:

  • invalid states,
  • forgotten invariants,
  • impossible transitions that became possible.

Lean lets you model systems where:

  • assumptions are explicit,
  • transitions are checked,
  • proofs accompany implementations.

A More Interesting Direction

A todo app becomes genuinely interesting once you add:

  • offline sync,
  • collaboration,
  • event sourcing,
  • permissions,
  • undo/redo,
  • conflict resolution.

Then you start proving:

  • merge convergence,
  • replay determinism,
  • permission safety,
  • index consistency.

At that point, you are doing miniature distributed systems research.

Final Thoughts

The important lesson is not:

“we proved a todo app correct”.

It is:

ordinary software contains hidden formal structure.

Most systems already behave like:

  • state machines,
  • transition systems,
  • protocol graphs,
  • logical constraint engines.

Lean simply forces those assumptions into the open.

And once they are explicit:
they become provable.

*AI agents write code fast. They also silently remove logic, change behavior, and introduce bugs -- without telling you. You often find out in production.

git-lrc fixes this. It hooks into git commit and reviews every diff before it lands. 60-second setup. Completely free.*

Any feedback or contributors are welcome! It's online, source-available, and ready for anyone to use.

GitHub logo HexmosTech / git-lrc

Free, Micro AI Code Reviews That Run on Commit



AI agents write code fast. They also silently remove logic, change behavior, and introduce bugs -- without telling you. You often find out in production.

git-lrc fixes this. It hooks into git commit and reviews every diff before it lands. 60-second setup. Completely free.

See It In Action

See git-lrc catch serious security issues such as leaked credentials, expensive cloud operations, and sensitive material in log statements

git-lrc-intro-60s.mp4

Why

  • 🤖 AI agents silently break things. Code removed. Logic changed. Edge cases gone. You won't notice until production.
  • 🔍 Catch it before it ships. AI-powered inline comments show you exactly what changed and what looks wrong.
  • 🔁 Build a…
View on GitHub

Top comments (0)