Number Theory

Infinitude of Primes

Euclid's classic proof that there are infinitely many prime numbers

Premier
lean4-proofnumber-theoryvisualization

Fundamental Theorem of Arithmetic

Every integer greater than 1 has a unique prime factorization

lean4-proofnumber-theoryvisualization

Fermat's Little Theorem

For prime p, a^p is congruent to a mod p

lean4-proofnumber-theorymodular-arithmeticvisualization

Quadratic Reciprocity

Relationship between solvability of quadratic congruences for two odd primes

lean4-proofnumber-theorymodular-arithmeticvisualization

Euclidean Algorithm

The oldest surviving algorithm, computing the greatest common divisor via iterated remainders

lean4-proofnumber-theoryalgorithmvisualization

Bezout's Identity

The gcd of two integers is always an integer linear combination of those integers

lean4-proofnumber-theorylinear-combinationsvisualization

Chinese Remainder Theorem

Simultaneous congruences with coprime moduli have a unique solution mod their product

lean4-proofnumber-theorymodular-arithmeticvisualization

Wilson's Theorem

A natural number p > 1 is prime if and only if (p-1)! ≡ -1 mod p

lean4-proofnumber-theoryprimalityfactorialsvisualization

Euler's Totient Function

φ(n) counts integers up to n coprime to n, and governs modular exponentiation

lean4-proofnumber-theorymodular-arithmeticgroup-theoryvisualization

Sum of Two Squares

A prime is a sum of two perfect squares if and only if it equals 2 or is congruent to 1 mod 4

lean4-proofnumber-theoryvisualization

Pythagorean Triples

Complete parametrisation of all integer solutions to a² + b² = c²

lean4-proofnumber-theoryvisualization

Lucas's Theorem

Binomial coefficients mod a prime p reduce digit-by-digit in base p

lean4-proofnumber-theoryvisualization

Möbius Inversion

If g equals the Dirichlet convolution of f with the constant 1, then f recovers via the Möbius function

lean4-proofnumber-theoryvisualization

Multiplicative Functions

Arithmetic functions that split over coprime inputs: f(mn) = f(m)f(n) when gcd(m,n) = 1

lean4-proofnumber-theoryvisualization

Quadratic Residues

An integer a is a quadratic residue mod p when it is a nonzero perfect square in Z/pZ

lean4-proofnumber-theoryvisualization

Legendre Symbol

The Legendre symbol (a|p) encodes whether a is a quadratic residue mod a prime p

lean4-proofnumber-theoryvisualization

Jacobi Symbol

The Jacobi symbol generalises the Legendre symbol to composite odd moduli

lean4-proofnumber-theoryvisualization

Primitive Roots

A primitive root mod p is a generator of the cyclic group (Z/pZ)*, existing for every prime p

lean4-proofnumber-theoryvisualization

Discrete Logarithm

The discrete logarithm is the inverse of modular exponentiation: find k such that g^k = a in a finite group

lean4-proofnumber-theoryvisualization

Continued Fractions

Every rational number has a finite continued fraction expansion; irrationals have infinite periodic ones

lean4-proofnumber-theoryvisualization

Order Modulo n

The multiplicative order of a mod n is the smallest positive k with a^k ≡ 1 (mod n), and it always divides phi(n)

lean4-proofnumber-theoryvisualization

Carmichael Numbers

Carmichael numbers are composite integers n satisfying a^n ≡ a (mod n) for all a, fooling Fermat's primality test

lean4-proofnumber-theoryvisualization

Pell's Equation

For non-square d, the equation x² - dy² = 1 always has infinitely many integer solutions

lean4-proofnumber-theoryvisualization

Lagrange's Four-Square Theorem

Every natural number is the sum of four perfect squares

lean4-proofnumber-theoryvisualization

Legendre's Three-Square Theorem

A positive integer is a sum of three squares iff it is not of the form 4^a(8b+7)

lean4-proofnumber-theoryvisualization

Bertrand's Postulate

For every positive integer n there is always a prime p with n < p ≤ 2n

lean4-proofnumber-theoryvisualization

Chebyshev's Bounds for π(n)

The prime counting function satisfies c₁·n/ln(n) ≤ π(n) ≤ c₂·n/ln(n) for explicit constants

lean4-proofnumber-theoryvisualization

Mertens' Theorems

The sum of reciprocals of primes diverges, with precise logarithmic asymptotics

lean4-proofnumber-theoryvisualization

Divisor Function σ(n)

The sum-of-divisors function σ(n) is multiplicative and characterises perfect numbers

lean4-proofnumber-theoryvisualization

Prime Counting Function π(n)

π(n) counts primes up to n and satisfies π(n) ~ n/ln(n) by the Prime Number Theorem

lean4-proofnumber-theoryvisualization