Fundamental theorem of arithmetic --- existence

Proved

FundamentalTheoremOfArithmetic.fta_existence

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

number-theoryprime-numbers

This is the existence half of the Fundamental Theorem of Arithmetic (Apostol, Introduction to Analytic Number Theory, 1976, Theorem 1.9): every nonzero natural number can be written as a product of primes.

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

Here $l$ ranges over multisets of natural numbers — a multiset is an unordered collection that tracks how many times each element occurs. The witnessing multiset $l$ need not be unique at this stage; that is the content of the companion uniqueness milestone. For $n = 1$ , the empty multiset witnesses the claim, since the empty product equals $1$ .

This lemma alone gives every nonzero integer some representation as a product of primes, without yet ruling out that a different product of primes could give the same value.

Formalization Note. The factorization is represented as Multiset ℕ, and l.prod denotes the product of its elements with multiplicity, under the convention that the empty multiset has product $1$ .

Preamble

import Mathlib

Formal statement

namespace FundamentalTheoremOfArithmetic
theorem fta_existence (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, Theorem 1.9

Read-back

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

This theorem is stated for a single natural number $n$ , together with the hypothesis $n \neq 0$ (so the zero case is excluded from the claim entirely). Under this hypothesis, the theorem asserts:

\exists\, l : \text{Multiset } \mathbb{N},\quad \left(\forall p \in l,\ p \text{ is prime}\right) \ \wedge\ \prod_{p \in l} p = n.

Concretely: there exists a multiset $l$ of natural numbers (a finite unordered collection allowing repeats) such that every element $p$ of $l$ satisfies Nat.Prime p --- Mathlib's standard primality predicate on $\mathbb{N}$ (asserting $p \geq 2$ and having no divisors other than $1$ and $p$ ) --- and such that the product of all elements of $l$ , taken in the commutative monoid $(\mathbb{N}, \times, 1)$ , equals $n$ . The product $\prod_{p\in l} p$ is Multiset.prod, i.e. the multiset elements multiplied together with multiplicity, under the convention that the product of the empty multiset is $1$ (so $l = \emptyset$ would only witness the case $n = 1$ ).

No claim of uniqueness is made: the statement is purely existential ( $\exists$ , not $\exists!$ ), so it does not assert that $l$ is the unique such multiset, nor does it say anything about the multiset being sorted, canonical, or related to any specific factorization algorithm. There is no claim about what happens when $n = 0$ ; that case is excluded by the hypothesis $hn : n \neq 0$ and the theorem is vacuously silent about it. The only free variable is $n : \mathbb{N}$ , universally quantified via the theorem's own argument binder, with $hn$ as the sole hypothesis; $l$ is existentially bound within the conclusion. No typeclass assumptions beyond the ambient structure of $\mathbb{N}$ and Multiset ℕ are used.

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