# Natural numbers

The `Nat` type represents the natural numbers, i.e., arbitrary-precision unsigned integers. There are no overflows.

``````#eval 100000000000000000 * 200000000000000000000 * 1000000000000000000000
``````

A numeral is considered to be a `Nat` if there are no typing constraints.

``````#check 10    -- Nat
#check id 10 -- Nat

def f (x : Int) : Int :=
x - 1

#eval f (3 - 5) -- 3 and 5 are `Int` since `f` expects an `Int`.
-- -3
``````

The operator `-` for `Nat` implements truncated subtraction.

``````#eval 10 - 5 -- 5
#eval 5 - 10 -- 0

theorem ex : 5 - 10 = 0 :=
rfl

#eval (5:Int) - 10 -- -5
``````

The operator `/` for `Nat` implements Euclidean division.

``````#eval 10 / 4 -- 2

#check 10.0 / 4.0 -- Float
#eval 10.0 / 4.0  -- 2.5
``````

As we described in the previous sections, we define the `Nat` type as an `inductive` datatype.

``````namespace hidden
inductive Nat where
| zero : Nat
| succ : Nat → Nat
end hidden
``````

However, the internal representation of `Nat` is optimized. Small natural numbers (i.e., < `2^63` in a 64-bit machine) are represented by a single machine word. Big numbers are implemented using GMP numbers. We recommend you use fixed precision numeric types only in performance critical code.

The Lean kernel has builtin support for the `Nat` type too, and can efficiently reduce `Nat` expressions during type checking.

``````#reduce 100000000000000000 * 200000000000000000000 * 1000000000000000000000

theorem ex
: 1000000000000000 * 2000000000000000000 = 2000000000000000000000000000000000 :=
rfl
``````

The sharp-eyed reader will notice that GMP is part of the Lean kernel trusted code base. We believe this is not a problem because you can use external type checkers to double-check your developments, and we consider GMP very trustworthy. Existing external type checkers for Lean 3 (e.g., Trepplein and TC) can be easily adapted to Lean 4. If you are still concerned after checking your development with multiple different external checkers because they may all rely on buggy arbitrary-precision libraries, you can develop your own certified arbitrary-precision library and use it to implement your own type checker for Lean.