Top 100 Mathematical Theorems

ImandraX is not just an environment for reasoning about programs — it is also a powerful interactive theorem prover for formalizing mathematics in its own right, with unique strengths due to its computational logic and industrial-strength proof and counterexample automation. As part of an ongoing project, Grant Passmore has formalized 20 theorems from Freek Wiedijk's celebrated "Formalizing 100 Theorems" list in ImandraX, positioning it alongside Lean, Coq, and Isabelle as a platform for mathematical reasoning.

Overview

Freek Wiedijk's list tracks which proof assistants have formalized 100 important mathematical theorems. This ongoing formalization effort covers a growing collection of results, spanning number theory, real analysis, combinatorics, geometry, and algebra.

All proofs are written in IML and verified using ImandraX's automated reasoning — combining the inductive waterfall, nonlinear arithmetic, and lightweight tactic guidance.

Theorem 1: Irrationality of √2

The proof that no rational number, when squared, equals 2. The argument proceeds via modular arithmetic: if p² = 2q² with gcd(p,q) = 1, then both p and q must be even — contradicting coprimality.

The proof builds through a chain of lemmas on squares modulo 2 and modulo 4:

theorem square_even_iff_even x =
  ((x * x) mod 2 = 0) = (x mod 2 = 0)
 
theorem square_mod4_even x =
  x mod 2 = 0 ==> (x*x) mod 4 = 0
 
theorem square_mod4_odd x =
  x mod 2 = 1 ==> (x*x) mod 4 = 1

These combine to show both p and q must be even:

theorem no_coprime_solution_p2_eq_2q2 p q =
  (gcd p q = 1 && p*p = 2*(q*q)) ==> false
[@@by [%use p_even_from_eq p q]
  @> [%use q_even_from_eq p q]
  @> [%use gcd_absorbs_common_divisor 2 p q]
  @> auto]

The final theorem lifts this to normalized rationals:

theorem sqrt2_is_irrational (r:Rational.t) =
  Rational.is_reduced r
  ==> Rational.square r <> Rational.of_int 2

Theorem 3: Denumerability of the Rationals

A constructive proof that the rationals are countable, using Cantor's pairing function as the foundation. The encoding maps each rational p/q to a natural number by encoding sign bits and absolute values via nested Cantor pairs:

let encode (q:Rational.t) : int =
  let n1,n2,n3,n4 = encode_terms q in
  let f = Cantor.cantor_pair in
  f (n1, f (n2, f (n3, n4)))

The key results about the Cantor pairing function itself:

theorem cantor_pair_onto n =
  let (a, b) = cantor_pair_inverse n in
  n >= 0 ==> a >= 0 && b >= 0 && cantor_pair (a, b) = n
 
theorem cantor_pair_one_one a b a' b' =
  a >= 0 && b >= 0 && a' >= 0 && b' >= 0
  && cantor_pair (a,b) = cantor_pair (a',b')
  ==> a = a' && b = b'

The main theorem establishes the surjection from ℕ to ℚ:

theorem rationals_denumerable_surj (q : Rational.t) =
  Bijection.surj decode encode
    (fun n -> n >= 0) (fun (_:Rational.t) -> true) q

Theorem 4: Pythagorean Theorem

Two formulations. The coordinate-level statement is purely polynomial in 6 reals:

theorem pythagoras_coords (ax:real) (ay:real) (bx:real) (by:real) (cx:real) (cy:real) =
  (* Right angle at C *)
  (((ax - cx) * (bx - cx) + (ay - cy) * (by - cy)) = 0.0)
  ==> (* |AB|² = |AC|² + |BC|² *)
  (((ax - bx) * (ax - bx) + (ay - by) * (ay - by))
    = ((ax - cx) * (ax - cx) + (ay - cy) * (ay - cy)
    + (bx - cx) * (bx - cx) + (by - cy) * (by - cy)))
[@@by auto]

The geometric version uses vector predicates over ℝ²:

theorem pythagoras (a : point) (b : point) (c : point) =
  right_at c a b ==> dist2 a b = Real.(dist2 a c + dist2 b c)
[@@by auto]

Both are fully automatic — auto handles the polynomial identity directly.

Theorem 11: Infinitude of Primes

Euclid's classic argument: for any n, the smallest divisor of n! + 1 is a prime greater than n. The proof requires several deep lemmas:

• prod_upto_mod_zero — every k ≤ n divides n!
• no_small_divisor_for_euclid_sum — no k ∈ [2..n] divides n! + 1
• sd_idempotent — the smallest-divisor function is idempotent (its output is prime)
• euclid_gt_n — the constructed prime exceeds n

theorem infinitude_of_primes n =
  let bigger_prime = euclid (abs n) in
  is_prime bigger_prime && bigger_prime > n
[@@by [%use euclid_is_prime (abs n)]
   @> [%use euclid_gt_n (abs n)] @> auto]

The idempotency theorem sd_idempotent is one of the deepest lemmas — it establishes that the smallest divisor of m is itself prime by showing that sd(sd(m)) = sd(m). This uses transitivity of divisibility and the strict minimality property.

Theorem 27: Triangle Interior Angles

An algebraic proof that the interior angles of any nondegenerate triangle sum to 180°. Without trigonometry, angles are represented as ordered pairs of nonzero vectors, with equality defined via the polynomial condition cos² θ₁ = cos² θ₂.

The construction draws a line through vertex A parallel to BC:

let d_point (a:point) (b:point) (c:point) : point = add a (sub c b)  (* AD = BC *)
let e_point (a:point) (b:point) (c:point) : point = add a (sub b c)  (* AE = -BC *)

The theorem witnesses three consecutive angles along this straight line that match the triangle's interior angles:

theorem triangle_interior_angles_sum_to_180 (a:point) (b:point) (c:point) =
  neqp a b && neqp b c && neqp c a && noncollinear a b c
  ==> angles_sum_to_straight
    (angB_u b a) (angB_v b c)
    (angA_u a b) (angA_v a c)
    (angC_u c a) (angC_v c b)
[@@by intros
  @> ... exists r1 r2 r3
  @> [%simp_only ...] @> nonlin ()]

The final step reduces to a polynomial identity discharged by nonlin().

Theorem 34: Divergence of the Harmonic Series

The proof that H(n) = 1 + 1/2 + ... + 1/n grows without bound. The key insight: each dyadic block [2^{k-1}+1 .. 2^k] contributes at least 1/2 to the sum.

theorem harmonic_extend_lower_bound_corollary k =
  k >= 1 ==> harmonic_extend (exp2 (k-1)) (exp2 k) >=. (1.0 /. 2.0)

This gives the lower bound H(2^k) ≥ 1 + k/2:

theorem harmonic_sum_lower_bound k =
  k >= 1 ==> harmonic_sum (exp2 k) >=. (1.0 +. (_R k /. 2.0))

Combined with monotonicity of H, this yields:

theorem harmonic_series_diverges m n =
  m >= 0 && n >= exp2 (2*m)
  ==> harmonic_sum n >. Real.of_int m

Theorem 42: Sum of Reciprocals of Triangular Numbers

A proof that ∑(1/T_k) = 2, where T_k = k(k+1)/2 is the k-th triangular number. The key is the telescoping identity:

lemma tri_term_telescopes k =
  (k > 0) ==> tri_term k = (_R 2) *. ((_R 1) /. (_R k) -. (_R 1) /. (_R (k + 1)))
[@@by intros @> simplify () @> nonlin ()]

The main theorem establishes the closed form S(n) = 2 - 2/(n+1):

theorem sum_of_reciprocals_of_triangular_numbers n =
  sum_recip_tri n = sum_recip_tri_closed n
[@@by induction () @>| [auto; intros @> ... @> nonlin ()]]

Theorem 44: Binomial Theorem

The binomial theorem (x+y)ⁿ = Σ C(n,k) xⁿ⁻ᵏ yᵏ proved by induction using Pascal's identity. The key combiner lemma distributes x and y over partial sums:

lemma binom_sum_step n k x y =
  k >= 0 && n >= 0
  ==> x * binom_sum n k x y + y * binom_sum n (k - 1) x y
      = binom_sum (n + 1) k x y

This itself requires induction, with interior cases using Pascal's identity and boundary cases using choose_out_of_range.

theorem binomial_theorem n x y =
  n >= 0 && x >= 0 && y >= 0
  ==> pow (x + y) n = binom_eval n x y

Theorem 52: Number of Subsets

A finite set with n elements has 2ⁿ subsets:

let rec powerset (xs:'a list) : 'a list list =
  match xs with
  | [] -> [[]]
  | x::xt -> let ps = powerset xt in ps @ (prepend x ps)
 
theorem powerset_len xs =
  List.length (powerset xs) = pow 2 (List.length xs)
[@@by auto]

Proved fully automatically — ImandraX discovers the induction and discharges all goals.

Theorem 54: Königsberg Bridges

Euler's theorem that no Eulerian path exists through the seven bridges of Königsberg. Two independent proofs are given.

Proof 1 — exhaustive symbolic enumeration:

theorem konigsberg_concrete start b1 b2 b3 b4 b5 b6 b7 =
  not (eulerian start b1 b2 b3 b4 b5 b6 b7)
[@@by unroll 50]

Proof 2 — a general parity argument via permutation-preserving occurrence counts:

theorem konigsberg r p =
  List.mem r regions && valid_path p r
  ==> not (permutation p bridges)
[@@by intros
  @> ... [%use parity_occurrences p r s]
  @> [%use permp_occurrences p bridges s]
  @> [%use parity_bridges s]
  @> esimp @> simplify ()]

Theorem 57: Cube Dissection Impossibility

A proof that a cube cannot be dissected into finitely many smaller cubes all of different sizes. The proof constructs an infinite descending sequence of cubes — each smaller than the last — using the "smallest cube touching the top face" operation, then applies the pigeonhole principle:

theorem no_dissection_exists cs t h0 =
  is_dissection cs && has_coverage cs t && List.mem h0 cs
  && cube_max Ax_Z h0 <. 1.0
  ==> false
[@@by [%use sequence_length cs h0 (List.length cs + 1)]
   @> [%use sequence_all_in_cs cs t h0 (List.length cs + 1)]
   @> [%use sequence_distinct_widths cs t h0 (List.length cs + 1)]
   @> [%use pigeonhole cs (build_sequence cs h0 (List.length cs + 1))]
   @> auto]

This is one of the most complex proofs in the collection, featuring 4 geometric axioms, a custom pigeonhole principle (itself proved from scratch), and extensive lemma chains about descending width sequences.

Theorem 58: Formula for Number of Combinations

The closed-form formula C(n,k) = n! / (k! · (n-k)!) proved in a division-free form:

theorem choose_times_factorials n k =
  (0 <= k && k <= n)
  ==> Binomial.choose n k * fact k * fact (n - k) = fact n

Then, using exact division:

theorem choose_closed_form n k =
  0 <= k && k <= n
  ==> Binomial.choose n k = fact n / (fact k * fact (n - k))

The proof uses Pascal's identity, factorial shift lemmas, and exact-division cancellation.

Theorems 60 & 69: Bézout's Theorem & GCD Algorithm

The Euclidean GCD algorithm and Bézout's theorem proved together. GCD is defined by subtraction:

let rec gcd (a:int) (b:int) : int =
  if a < 0 || b < 0 then 0
  else if a = 0 then b
  else if b = 0 then a
  else if a >= b then gcd (a - b) b
  else gcd a (b - a)

Bézout coefficients are computed by a parallel recursion:

let rec bezout_sub (a:int) (b:int) : int * int =
  ...
  else if a >= b then
    let (u',v') = bezout_sub (a - b) b in (u', v' - u')
  else
    let (u',v') = bezout_sub a (b - a) in (u' - v', v')
 
theorem bezout a b =
  let (u,v) = bezout_sub a b in u*a + v*b = gcd a b
[@@by auto]

Key derived properties include gcd_dvd_both_pos, gcd_absorbs_common_divisor, and the coprimality-of-squares lemma gcd_square_square_from_coprime.

Theorem 65: Isosceles Triangle Theorem

If two sides of a triangle are equal, the opposite angles are equal. Angles are represented as polynomial relations (cos² equality):

theorem isosceles_triangle (a:point) (b:point) (c:point) =
  neqp a b && neqp a c && dist2 a c = dist2 b c
  ==> angle_eq (sub c a) (sub b a) (sub a b) (sub c b)
[@@by [%simp_only neqp,sub,angle_eq,norm2,dot,dist2]
   @>>| ... @> nonlin ()]

The proof normalizes all geometric definitions to polynomial form and finishes with nonlin().

Theorem 74: Principle of Mathematical Induction

A meta-theorem: given axioms for base and inductive step, prove prop n for all n ≥ 0. The proof uses a minimal-counterexample argument:

axiom base prop = prop 0
axiom inductive prop n = n >= 0 && prop n ==> prop (n+1)
 
theorem induction prop n =
  n >= 0 ==> prop n
[@@by intros
  @> ... [%use counterexample_outcome prop 0 n]
  @> [%cases c = -1, c >= 1]
  @>| [... [%use counterexample_neg1_means_k_holds prop 0 n] @> auto;
       ... [%use inductive prop (c-1)] @> simplify ();
       arith]]

Theorem 78: Cauchy-Schwarz Inequality

Proved in two forms over arbitrary-dimension real vectors:

Form 1: ⟨u,v⟩² ≤ ⟨u,u⟩⟨v,v⟩

theorem cauchy_schwarz_1 u v =
  same_length u v ==>
  Real.(dot u v * dot u v) <=. Real.(dot u u * dot v v)

Form 2: |⟨u,v⟩| ≤ ‖u‖ ‖v‖ (using a relational sqrt)

theorem cauchy_schwarz_2 u v eu ev =
  same_length u v && is_sqrt eu (norm_sq u) && is_sqrt ev (norm_sq v)
  ==> abs_real (dot u v) <=. Real.(eu * ev)

The proof proceeds via the optimal projection formula: ‖u - tv‖² ≥ 0 with t = ⟨u,v⟩/⟨v,v⟩ gives the inequality directly. Key lemmas include sqrt monotonicity, norm-squared non-negativity, and the algebraic simplification of the projection residual.

The equality condition (linear dependence) is also established:

lemma linear_dependence_implies_equality a v =
  Real.(dot (scalar_mult a v) v * dot (scalar_mult a v) v)
  = Real.(norm_sq (scalar_mult a v) * norm_sq v)

Theorem 80: Fundamental Theorem of Arithmetic

Every integer ≥ 2 has a unique prime factorization. The proof has two parts.

Existence — by strong induction, factoring via the smallest divisor:

let rec prime_factors (n:int) : int list =
  if n < 2 then []
  else let d = small_divisor_from 2 n in
    if d = n then [n] else (prime_factors d) @ (prime_factors (n / d))
 
theorem prime_factorization_exists n =
  n >= 2 ==> all_prime (prime_factors n) && prod_list (prime_factors n) = n

Uniqueness — using Euclid's lemma (if p | ab then p | a or p | b, proved via Bézout) and multiset permutation:

theorem prime_factorization_unique xs ys =
  all_prime xs && all_prime ys && prod_list xs = prod_list ys
  ==> permutation xs ys

This is one of the largest proofs in the collection, building on Bézout's theorem, the GCD development, and a bespoke prime_mem_if_divides_prod lemma chain.

Theorem 85: Divisibility by 3 Rule

An integer is divisible by 3 if and only if the sum of its digits is divisible by 3:

theorem divisibility_by_3_rule n =
  (n >= 0) ==> ((n mod 3 = 0) = (sum_digits n mod 3 = 0))
[@@by [%use sum_digits_preserves_mod3 n] @> auto]

The core congruence sum_digits_preserves_mod3 is proved by induction, using the distribution of mod over addition and the fact that 10 ≡ 1 (mod 3).

Theorem 91: Triangle Inequality

‖u + v‖ ≤ ‖u‖ + ‖v‖ over ℝ², building on Cauchy-Schwarz:

theorem triangle_inequality (x:R2.vec) (y:R2.vec) (nx:real) (ny:real) (nxy:real) =
  nx >= 0.0 && ny >= 0.0 && nxy >= 0.0
  && nx * nx = norm x && ny * ny = norm y && nxy * nxy = norm (add x y)
  ==> nxy <= nx + ny

The proof chains together Cauchy-Schwarz, sum-of-squares expansion, and an "unsquaring" lemma that extracts the inequality from its squared form.

Summary

References

• Source: imandra-100-theorems
• Freek Wiedijk's 100 Theorems list