Lean examples

Run a program, check a proof, and find your way around leanlab.

Compute an answer, then prove the equality.

A proposition is a type; a proof is a term of that type.

Define a function and print its result from main.

Evaluate expressions with #eval and inspect their types with #check.

Functions take inputs and return values. Application uses spaces, so parentheses group expressions.

Turn the mathematical definition of Fibonacci numbers into a recursive program.

Build a small data pipeline with immutable lists and higher-order functions.

Describe a small set of possibilities and handle each one explicitly.

Group named fields into your own data type, then write a function that uses it.

Option makes missing values explicit, so the compiler helps you handle both outcomes.

Lean checks that ordinary recursive definitions terminate.

Use Except and do to return a value or an explanation of failure.

Build an array and access an element with a checked bound.

Write one function whose behavior depends on the input type.

A theorem is a declaration whose type is a proposition. Lean checks the supplied proof.

Use assumptions to construct proofs. An implication is a function from one proof to another.

Prove a property for all natural numbers using a base case and a successor case.

Write a function, prove a property about it, and execute it in the same file.

See the warning for an admitted statement, then replace the placeholder.

Simplify expressions with library lemmas and selected definitions.

Name intermediate facts and justify each step of an equality.

Read quantified statements and construct their proofs.

Relate a square-area identity to a² + b² = c², then check an exact right-triangle example.

Prove Euclid’s identity for arbitrary integer parameters, then generate several Pythagorean triples.

A nonnegative square is enough to explain why the arithmetic mean dominates the geometric mean.

Expand a square and a cube. Lean’s core grind tactic normalizes polynomial expressions.

A matrix satisfies its own characteristic polynomial. Unpack that statement into four scalar identities.

Avoid floating-point square roots: verify the squared area with exact natural-number arithmetic.

Prove a familiar summation formula with recursion and induction.

A small recursive function and an induction proof of the triangular-number formula.

Repeat the induction pattern with a slightly richer polynomial.

A famous inequality becomes a nonnegative square after one algebraic identity.

Express the factor theorem directly, without importing a polynomial library.

Derive the numerators in the formula for solving two simultaneous linear equations.

Discover the algebra behind the quadratic formula, then prove exactly which integers solve x²−5x+6=0.

Every unit modulo 10 raised to the fourth power returns to 1. Exhaust a finite type with a kernel-checked proof.

Build a search program, then supply an explicit witness that Lean checks independently.

Turn one integer solution into another, and prove the transformation preserves the equation.

Compute (p−1)! modulo p and recognize the residue −1.

Negative coefficients let a linear combination of two positive integers equal 1. Supply a certificate Lean can check.

Run an ancient algorithm and reuse its verified properties in your own theorem.

Compute divisors, sum them, and check the first two perfect numbers.

Prove the single step behind a familiar school arithmetic trick.

Import a core module, reuse a library theorem, and prove a concrete large-number GCD equality.

Build every binary membership pattern and prove its count by induction.

Compute the parity obstruction behind the seven-bridges puzzle.

A recursive program mirrors the two cases in a combinatorial proof.

An infinite theorem with a short proof: build a predicate that cannot appear in any proposed complete list.

State the principle itself as a theorem, with a base case and a step supplied as arguments.

Addition and multiplication can obey ring laws even when division by a nonzero element is impossible.

Prove that arithmetic modulo 5 forms a field by checking every possible input.

Construct a Galois field yourself, then let Lean exhaustively verify its addition, multiplication, and inverses.

Run both sides of a key exchange and prove they arrive at the same residue.

Use a finite type to prove a complete round trip for every message in a miniature RSA system.

Use Lean’s built-in hash and see why a hash match is not proof of equality.

Compute SHA-256 digests using the implementation included in this file.

Compute BLAKE3 digests with a self-contained implementation of its compression function and chunk tree.

Prove a concrete list length by reducing a decision procedure.

Prove the same list length without computing the list.

Write two equivalent sums and prove the accumulator invariant.