Making a “Hello World” in Lean

If you're not a Medium member, a video version is available on YouTube.

Not so long time ago, in September 2026, OpenAI claimed that they solved one of the Millennium Prize math problems — the Navier–Stokes equations, describing the motion of viscous fluids. What is interesting for us, the proof was written in the programming language Lean, and it is available on GitHub.

As a software developer, I had never used Lean before, but after reading the news, I became curious about how it works. And I decided to make a simple "Hello World" in Lean and also to prove two simple school-level theorems.

Let's get started! If you're interested in the coding process "in action," a video is also added at the end of the article.

1. The Pythagorean Theorem

Let's start with something simple — the Pythagorean theorem. It is simple, and hopefully everyone knows it. Let's say we have a right triangle:

The Pythagorean theorem states that:

C² = A² + B²

If you made at least one computer game, you probably used this formula a lot to get the distance between two points.

How can we prove it in Lean?

First, Lean will not prove the theorem for us. But it can verify the proof. So, first, we need to create a proof on our own. For the Pythagorean theorem, it is easy. Let's add four triangles and a square of side length C:

Then the area of the full square is (A + B)². It is also equal to the area of the internal square C² plus four triangles with an area of 1⁄2AB each. Then we can write all this together:

S = (A + B)² = (A + B)(A + B) = A² + 2AB + B² S = C² + 4*1⁄2AB = C² + 2AB C² + 2AB = A² + 2AB + B² => C² = A² + B²

I hope it looks simple enough. But imagine a large theorem with a 5-page proof. Can we code it formally in a programming language, so the computer can verify that it's correct? Indeed, we can, and this is exactly what Lean was designed for!

Visually, it looks a bit like Python, and first I need to import the libraries:

import Mathlib.Basic.Real.Basic
import Mathlib.Tactic.Ring

import Mathlib.Basic.Real.Basic
import Mathlib.Tactic.Ring

Here, Ring is a math solver that can simplify formulas, expand brackets, and do other routine algebra stuff. And Real is a basic data type for real numbers. Now, we can declare a theorem:

theorem pythagoras_algebra (
  a b c : Real
) (h : c^2 = (a + b)^2 - 4 * (a * b / 2)) : c^2 = a^2 + b^2 := by

theorem pythagoras_algebra (
  a b c : Real
) (h : c^2 = (a + b)^2 - 4 * (a * b / 2)) : c^2 = a^2 + b^2 := by

Here, a, b, and c are the data inputs; c² = (a + b)² — 4 * (a * b / 2) is a hypothesis I have, and c² = a² + b² is a consequence of this hypothesis that I want to prove.

Now, I can write the actual body:

  calc
    c^2 = (a + b)^2 - 4 * (a * b / 2) := h
    _   = a^2 + 2 * a * b + b^2 - 2 * a * b := by ring
    _   = a^2 + b^2 := by ring

  calc
    c^2 = (a + b)^2 - 4 * (a * b / 2) := h
    _   = a^2 + 2 * a * b + b^2 - 2 * a * b := by ring
    _   = a^2 + b^2 := by ring

Here, I write equations line by line, and a keyword by allows Lean to know that the Ring solver can check this. For example, it can verify that (a + b)² — 4 * (a * b / 2) is indeed equals to a² + 2 * a * b + b² — 2 * a * b.

Everyone can try Lean online in 5 minutes at https://live.lean-lang.org by pasting the full code:

Here, the Lean output on the right shows "No goals," which means that all parts of the theorem are proved. And in the case of any math error, Lean will stop and show you the message.

Now, we can see the final point. If we can write a theorem in Lean, then the verification of the proof can be done automatically. The proof code can also be published, shared in a codebase, used to prove other theorems, and so on.

2. Half-Circle's Length

Now, let's try something different but also fun. What do you think, which curve is longer, black or blue?

Let's prove with Lean that they are equal. First, the length of the circle is 2πR, so the length of the black line is π(A + B)/2, and the total length of the blue lines is πA/2 + πB/2. Thus, we can write:

L1 = π(A + B)/2 L2 = πA/2 + πB/2

Hopefully, for everyone who attended at least a single math lesson at school, it's clear that L1 = L2. Let's write it in Lean:

theorem circles (
    a b l1 l2: Real
) (h1 : l1 = π * (a + b) / 2) (h2 : l2 = π * a  / 2 + π * b / 2) : l1 = l2 := by
  -- Substitute l1, goal is: π * (a + b) / 2 = l2
  rw [h1]
  rw [h2]
  ring

theorem circles (
    a b l1 l2: Real
) (h1 : l1 = π * (a + b) / 2) (h2 : l2 = π * a  / 2 + π * b / 2) : l1 = l2 := by
  -- Substitute l1, goal is: π * (a + b) / 2 = l2
  rw [h1]
  rw [h2]
  ring

Here, a rw (rewrite) keyword tells Lean to replace h1 with its definition π * (a + b) / 2 . The same works for h2. Then we call the Ring solver to verify that both equations are equal.

We can run the code in Lean, and the system shows "no goals". The proof is correct:

3. Making a "Hello World"

As we can see, we can prove the theorems in Lean. But can we also make and run the "classical" app? Indeed, we can. First, I will create a project named "triangle":

lake init triangle

lake init triangle

This syntax was probably inspired by make. As an example, I will create a method to check if all triangle values are correct:

def test_triangle (a b c : Int) : IO Unit := do
  -- The '==' checks for boolean equality at runtime
  if a^2 + b^2 == c^2 then
    IO.println s!"Success: {a}^2 + {b}^2 = {c}^2 is TRUE"
  else
    IO.println s!"Wrong: {a}^2 + {b}^2 = {c}^2 is FALSE"

def test_triangle (a b c : Int) : IO Unit := do
  -- The '==' checks for boolean equality at runtime
  if a^2 + b^2 == c^2 then
    IO.println s!"Success: {a}^2 + {b}^2 = {c}^2 is TRUE"
  else
    IO.println s!"Wrong: {a}^2 + {b}^2 = {c}^2 is FALSE"

The language looks like a weird mix of Python and Turbo Pascal, but why not? Now, we can add a "main" function and test 2 triangles:

def main : IO Unit := do
  IO.println "Testing numbers..."

  -- This will print Success
  test_triangle 3 4 5

  -- This will print Wrong
  test_triangle 4 5 6

def main : IO Unit := do
  IO.println "Testing numbers..."

  -- This will print Success
  test_triangle 3 4 5

  -- This will print Wrong
  test_triangle 4 5 6

Finally, we can build the project by running lake build and execute it by running the command lake exe triangle. And as we can see, the app works:

Apparently, Lean also has a GUI library, so theoretically it can run Doom — readers are welcome to check on their own :)

Conclusion

In this article, I tested the programming language Lean. As a software developer, I will probably never use it in production, as well as most other readers. Still, it was fun to test Lean and to see how it works. If you want to see the coding process "in action," you're also welcome to watch the video:

Embedded content

And if you're interested in solving math problems with code, you are also welcome to read another article:

This Math Problem Is 3,000 Years Old — Magic Squares Can My PC Solve It with C++, OpenMP, and CUDA?

If you enjoyed this story, press the "Like" button — it helps me to know if particular topics are interesting to readers or not. If you want to see more stories, use the "Follow" or "Subscribe" buttons, and you will get a notification when the next article is published. The full source code for this article is available on my Patreon page — your support may help me to write more articles like this.

Thanks for reading.