blog :: Brent -> [String] - Proving the Fundamental Theorem of Arithmetic in Agda<br>-->
Home •<br>About •<br>RSS •<br>BlogLiterately •<br>Catsters Guide •<br>How To Print<br>Things •
« Disco Live!
Proving the Fundamental Theorem of Arithmetic in Agda
Posted on June 26, 2026
Tagged agda, arithmetic, theorem, proof, Agda
Share on
tl;dr : This is a fully commentated, from-scratch proof of the<br>Fundamental Theorem of Arithmetic in<br>Agda,<br>intended for those who already know a bit of Agda but might benefit<br>from reading and working through a larger example. See the<br>Introduction and the Table of Contents below for more details.
Introduction
Earlier this spring, I was idly brainstorming potential final projects<br>for my Functional Programming<br>students. Having just taught my Discrete Math students the<br>Fundamental Theorem of<br>Arithmetic, I<br>wondered whether formalizingI mean formalizing it from scratch: of<br>course, the FTA is already in the Agda standard library. As I later<br>learned, it was added to the standard library by Nathan van Doorn,<br>aka Taneb.
it in<br>Agda<br>could make a nice project.
So I decided to spend about an hour trying to prove it in Agda,<br>to gauge the level of the project. At the end of an hour, I had<br>learned two things: (1) proving the Fundamental Theorem of Arithmetic is not an appropriate project for<br>my students (who had only had a few weeks’ practice with Agda); (2) I<br>was not going to be able to stop until I finished the proof myself!
Over the next week or so, I finished the proof completely from<br>scratch—without using anything from the standard library, and without<br>looking up any reference material. I based it only on my experience<br>in Agda, knowledge of the relevant proofs on an informal level, and<br>Agda techniques I’ve picked up along the way (from e.g. Conor McBride, Jacques<br>Carette, colleagues at Penn, and elsewhere).
I decided to publish the proof, with extra commentary, in the hopes<br>that it can be useful as an intermediate-level reference. That is,<br>perhaps you’ve learned some basic Agda (if not, I suggest this<br>tutorial to<br>start)<br>and have some basic familiarity<br>with the Curry-Howard correspondence, but would benefit from seeing an<br>example of a fully worked out, medium-sized proof.Another good<br>source of information along these lines is this post by Jesper<br>Cockx.
The resulting blog<br>post is extremely long, but I make no apologies for that—if you want<br>an entertaining 5-minute read, you should look elsewhere!
The entire blog post and proof is available as a literate Agda<br>document. Even better, I have also published another version of this<br>blog post with holes in place of almost all the proofs. For a<br>maximal learning experience, I suggest downloading it and trying to<br>fill in the holes yourself as you go along.
Below is a table of contents. Depending on your background, you may<br>of course choose to skip some sections. For example, if you have<br>already had a good deal of practice dealing with basic natural number<br>arithmetic, equality, and inequality in Agda, you might wish to skip<br>over those sections.
Table of Contents
Introduction
(Half of) The Fundamental Theorem of Arithmetic (Constructively)
Preliminaries
Basic logic
Equality
Natural numbers
No confusion
Decidable equality
Addition
Multiplication
Inequality
Relationships among equality and inequality
Arithmetic and inequality
Divisibility, primes, and composites
Nontrivial divisors come in pairs
Division
Absolute difference
Quotient and remainder are unique
The division algorithm, take 1
Construct the evidence you would like to pattern-match on
Well-founded induction
Accessibility
Well-founded induction, defined
Less-than is well-founded
The division algorithm
Primality testing
Counting up
Primality testing by trial division
Lists
The Fundamental Theorem of Arithmetic
Further Directions
(Half of) The Fundamental Theorem of Arithmetic (Constructively)
The Fundamental Theorem of<br>Arithmetic<br>(FTA for short) states that any natural number \(n \geq 1\) can be<br>written as a product of zero or more primes, and moreover that this<br>product is unique up to permutation.
For now, we are only going to prove the existence part (I may write<br>another blog post with the uniqueness proof later). Since a constructive<br>existence proof is really an algorithm for constructing the thing that<br>is claimed to exist, this can also be seen as a formally verified<br>factorization program: put any number in, get a prime factorization<br>out. Writing a prime factorization program is not hard, of course;<br>it’s the formal verification part that is interesting!
Stop! Before reading on, if you want to get the most out of this tutorial, I<br>strongly recommend downloading the version with<br>holes<br>and trying to complete as many of the proofs as you can before reading mine!
Preliminaries
We will often make use of A and B to stand for arbitrary<br>sets/types, so we use a variable declaration to tell Agda that it<br>should implicitly quantify them whenever they show up as free<br>variables....