Proving the fundamental theorem of arithmetic in Agda

The author (Brent Yorgey) is a computer scientist at Hendrix College and a core contributor to the Haskell functional-programming community. Agda is a dependently typed functional programming language and proof assistant — a tool where you write programs that are also mathematical proofs, and the compiler checks their correctness. The "fundamental theorem of arithmetic" (FTA) is the standard number-theory result that every positive integer has a unique prime factorization; proving it rigorously is notoriously subtle, especially the uniqueness part. This post demonstrates how to encode that proof in Agda's type system, making the computer verify every logical step. It matters because it shows how far "proof by programming" has come: even classical, non-trivial theorems can be machine-checked in an elegant, readable style.