Fundamental theorem of arithmetic

Proved

FundamentalTheoremOfArithmetic.fundamental_theorem_of_arithmetic

by Mayank Kumar · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryprime-numbers

The Fundamental Theorem of Arithmetic states that every nonzero natural number $n$ has exactly one factorization into primes, once factorizations that differ only in the order of their factors are identified.

\forall\, n \neq 0,\quad \exists!\, l,\quad (\forall p \in l,\ p \text{ is prime}) \ \wedge\ \prod_{p \in l} p = n.

A factorization is represented as a multiset $l$ of natural numbers — an unordered collection tracking multiplicity — all of whose elements are prime, whose product $\prod_{p \in l} p$ (with the empty product equal to $1$ ) recovers $n$ . The theorem asserts both that such an $l$ exists and that it is the only one: any other multiset of primes with product $n$ must equal $l$ .

For $n = 1$ the unique witness is the empty multiset; every $n \geq 2$ has a nonempty multiset of prime factors. This single result underlies essentially all of elementary number theory: it makes $\gcd$ , $\mathrm{lcm}$ , and multiplicative arithmetic functions well defined in terms of "the" prime factorization of an integer.

Formalization Note. Uniqueness is stated up to reordering by using Multiset rather than List, so no separate permutation argument is needed in the statement itself. This goal decomposes into the mission's two milestones: existence and uniqueness.

Preamble

import Mathlib

Formal statement

namespace FundamentalTheoremOfArithmetic
theorem fundamental_theorem_of_arithmetic (n : ℕ) (hn : n ≠ 0) :
    ∃! l : Multiset ℕ, (∀ p ∈ l, p.Prime) ∧ l.prod = n := by sorry
end FundamentalTheoremOfArithmetic

Source

T. M. Apostol, Introduction to Analytic Number Theory, Springer, 1976, Theorems 1.9-1.10 (combined); G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Theorem 2

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

For the natural number $n$ (with hypothesis $n \ne 0$ ), the theorem asserts the existence of a unique multiset $l$ of natural numbers such that (a) every element $p$ of $l$ (i.e. every $p$ with $p \in l$ , counted without regard to multiplicity duplication semantics of multisets) satisfies Nat.Prime $p$ --- Mathlib's standard primality predicate on $\mathbb{N}$ , true exactly for $p \ge 2$ with no divisors other than $1$ and $p$ --- and (b) the product of the elements of $l$ , taken with multiplicity, under the natural-number multiplication commutative monoid, equals $n$ ; and moreover this $l$ is unique in the sense that any other multiset $l'$ of natural numbers satisfying both conditions (a) and (b) (with $n$ ) must equal $l$ as a multiset. Concretely, "exists unique" here unfolds to:

\exists\, l : \mathrm{Multiset}\ \mathbb{N},\ \Big(\big(\forall p \in l,\ p.\mathrm{Prime}\big) \wedge l.\mathrm{prod} = n\Big) \wedge \forall\, l' : \mathrm{Multiset}\ \mathbb{N},\ \Big(\big(\forall p \in l',\ p.\mathrm{Prime}\big) \wedge l'.\mathrm{prod} = n\Big) \to l' = l.

Here $l.\mathrm{prod}$ denotes the product over the multiset $l$ (with repetition), where by convention the product of the empty multiset is $1$ ; so if $l$ were empty, the second conjunct would force $n = 1$ . The multiset $l$ is a priori an arbitrary finite multiset of natural numbers (no a priori bound on its cardinality or on the size of its elements), constrained only by primality of every member and by the product condition; note that since $n \ne 0$ but $n = 1$ is permitted (with $l = \emptyset$ , the empty multiset, being the unique witness in that case, since $1$ has no prime factors and any nonempty multiset of primes has product $\ge 2$ ), the hypothesis $n \ne 0$ does not rule out this degenerate case, only $n = 0$ (for which no such $l$ could exist, since no multiset of natural numbers --- being a product of nonnegative integers each $\ge 2$ , or the empty product $1$ --- can have product $0$ ). The theorem is stated for a single fixed $n : \mathbb{N}$ with the single hypothesis $n \ne 0$ , and there are no other explicit or implicit arguments, and no typeclass assumptions beyond those already built into the ambient Multiset, Nat, and their multiplication/primality structure from Mathlib.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by Mayank Kumar · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph