Best Practices

Writing idiomatic Lean 4 code requires more than just knowing syntax. Follow these guidelines to write code that is readable, maintainable, and aligned with the community.

Naming Conventions

Lean follows specific casing rules. Sticking to these makes your code look native.

• UpperCamelCase for types, structures, classes, namespaces, and modules.
  Example: Nat, HashMap, BinaryTree, ToString
• lowerCamelCase for functions, definitions, and local variables.
  Example: myFunction, calculateSum, isPrime, List.map
• snake_case for theorem and lemma names, describing the statement rather than naming it arbitrarily.
  Example: Nat.add_comm, Nat.succ_le_succ, List.length_append

Naming Theorems: the Mathlib Convention

A theorem name describes its conclusion, reading left to right, using standard abbreviations for the symbols. Once you internalise the scheme you can often guess the name of a lemma you need — which is far faster than searching.

1-- The name spells out the statement:
2theorem add_comm (a b : Nat) : a + b = b + a          -- "add is comm(utative)"
3theorem length_append : (as ++ bs).length = ...        -- "length of append"
4theorem succ_le_succ : n ≤ m → n.succ ≤ m.succ         -- hypothesis → conclusion
5
6-- Common vocabulary:
7--   _eq_    for =        _le_    for ≤        _lt_   for <
8--   _ne_    for ≠        _mem_   for ∈        _sub_  for ⊆
9--   _add_   for +        _mul_   for *        _neg_  for -x
10--   _iff_   for ↔        _not_   for ¬        _of_   for "follows from"
11--
12-- So: le_of_lt   : a < b → a ≤ b        ("≤ follows from <")
13--     not_lt_of_ge : a ≥ b → ¬(a < b)
14--     mul_le_mul_of_nonneg_left ...     (long names are GOOD here)

Explicit vs Implicit Types

Lean's type inference is powerful, but readability is king.

Do Type:

• Top-level function signatures (always!)
• Structure fields
• Ambiguous literals (e.g., (5 : Float))

1-- Good: explicit types for top-level
2def add (x : Nat) (y : Nat) : Nat := x + y
3
4-- Bad: relying on inference for public API
5def add x y := x + y   -- this does not even compile: Lean cannot infer x's type

Don't Type:

• Local variables where type is obvious
• Match arms where patterns imply types

Do Notation Usage

Use do notation for monadic code (IO, Option, etc.). Avoid raw bind (>>=) operators unless the pipeline is very short (1-2 steps).

1-- Good: readable, imperative style
2def safeCompute (x : Nat) : Option Nat := do
3  let y ← safeSubtract x 10
4  let z ← safeDivide y 2
5  return z
6
7-- Avoid: confusing operator chains for complex logic
8def hardToRead (x : Nat) : Option Nat :=
9  safeSubtract x 10 >>= fun y => safeDivide y 2 >>= fun z => pure z

Termination

Avoid partial unless absolutely necessary.partial functions cannot be used in proofs and can hide infinite loops. Try to use structural recursion or termination_by first.

Structure vs Class

Pattern Matching

Prefer the dot syntax match x with or the function match shorthand when possible.

1-- Good: shorthand for simple cases
2def isZero : Nat → Bool
3  | 0 => true
4  | _ => false
5
6-- Good: name only the fields you need, with .. for the rest
7structure Point where
8  x : Int
9  y : Int
10
11def getX (p : Point) : Int :=
12  match p with
13  | { x, .. } => x
14
15-- Better still: just use the accessor
16def getX' (p : Point) : Int := p.x

Use the Standard Library

Before writing a helper function, check List, Array, and String namespaces. Functions like filterMap,find?, any, and all are often built-in.