Imandra proofs of the "top 100" theorems :-)

This is a project by Grant Passmore to prove the Top 100 Theorems in Imandra.

Status

Currently, we have proven 17/100:

1. Irrationality of √2
3. Denumerability of the Rationals
4. Pythagorean Theorem
11. Infinitude of Primes
34. Divergence of the Harmonic Series
42. Sum of the Reciprocals of the Triangular Numbers
44. Binomial Theorem
52. Number of Subsets of a Set
54. Königsberg Bridges Problem
58. Formula for Number of Combinations
60. Bezout's Theorem
65. Isosceles Triangle Theorem
69. Greatest Common Divisor Algorithm
74. Principle of Mathematical Induction
80. The Fundamental Theorem of Arithmetic
85. Divisibility by 3 Rule
91. The Triangle Inequality

More coming soon!

Statements of the Theorems in Imandra

1. Irrationality of √2

Source: src/sqrt2_irrational.iml

Statement (informal): There does not exist $p\in\mathbb{Q}$ s.t. $p^2=2$.

Imandra statement

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

Back to list

3. Denumerability of the Rationals

Source: src/q_denum.iml

Statement (informal): There is a surjection from $\mathbb{N}$ to $\mathbb{Q}$.

Imandra statement

theorem decode_onto (q:Rational.t) =
  decode (encode q) = q

theorem rationals_denumerable_surj (q : Rational.t) =
  Bijection.surj
    decode
    encode
    (fun (n:int) -> n >= 0)       (* dom on N *)
    (fun (_:Rational.t) -> true)  (* all rationals allowed *)
    q

Back to list

4. Pythagorean Theorem

Source: src/pythagoras.iml

Statement (informal):

If the triangle $\triangle ABC$ is right-angled at vertex $C$, then $$|AB|^2 = |AC|^2 + |BC|^2.$$

Imandra statement

theorem pythagoras (a : point) (b : point) (c : point) =
  right_at c a b ==> dist2 a b = Real.(dist2 a c + dist2 b c)

Back to list

11. Infinitude of Primes

Source: src/inf_primes.iml

Statement (informal): There are infinitely many prime numbers.

Imandra statement

theorem infinitude_of_primes n =
  let bigger_prime = euclid (abs n) in
  is_prime bigger_prime && bigger_prime > n

Back to list

34. Divergence of the Harmonic Series

Source: src/harmonic.iml

Statement (informal):
The harmonic series diverges: its partial sums grow without bound.

More precisely, let

$$ H(n) = 1 + \frac{1}{2} + \frac{1}{3} + \cdots + \frac{1}{n}. $$

Then, $\forall m \ge 0$, if $n \ge 2^{2m}$ then $H(n) > m$.

Imandra statement

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

Back to list

42. Sum of the Reciprocals of the Triangular Numbers

Source: src/triangular.iml

Statement (informal):

The sum of the reciprocals of the triangular numbers converges to $2$.

More formally, for all $n \ge 0$, the partial sum of the reciprocals of the first $n$ triangular numbers satisfies

$$ \sum_{k=1}^{n} \frac{1}{T_k} = 2 - \frac{2}{n+1}, $$

where $T_k = \dfrac{k(k+1)}{2}$.

Imandra statement

theorem sum_recip_tri_closed_form n =
  n >= 0
  ==>
  sum_recip_tri n = 2.0 -. (2.0 /. (Real.of_int (n+1)))

Back to list

44. Binomial Theorem

Source: src/binomial.iml

Statement (informal):

For all $n \in \mathbb{N}$,

$$ (x + y)^n = \sum_{k=0}^{n} \binom{n}{k} x^{n-k} y^{k}. $$

Imandra statement

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

Back to list

52. Number of Subsets of a Set

Source: src/num_subsets.iml

Statement (informal): If $S$ is finite, then $|\mathcal{P}(S)|=2^{|S|}$.

Imandra statement

theorem powerset_len xs =
  List.length (powerset xs) = pow 2 (List.length xs)

Back to list

54. Königsberg Bridges Problem

Source: src/konigsberg.iml

Statement (informal):
The Königsberg Bridges Problem asks whether it is possible to take a walk through the city of Königsberg that crosses each of its seven bridges exactly once and returns to its starting point.

Euler showed that such a walk is impossible. In modern graph-theoretic terms, the corresponding graph has more than two vertices of odd degree, and thus has no Eulerian path.

We prove two versions:

• a concrete version, representing the specific Königsberg map and a purported (impossible) path of length 7 directly, which Imandra proves automatically, and
• a general version, using the abstract notion of Eulerian polarity and reasoning over permutations of edges, and then instantiating this to the configuration of Königsberg.

Imandra statement

theorem konigsberg_concrete start b1 b2 b3 b4 b5 b6 b7 =
  not (eulerian start b1 b2 b3 b4 b5 b6 b7)

theorem konigsberg r p =
  List.mem r regions && valid_path p r
  ==> not (permutation p bridges)

58. Formula for Number of Combinations

Source: src/combinations.iml

Statement (informal):

For integers $0\le k\le n$, $\displaystyle \binom{n}{k}=\frac{n!}{k!(n-k)!}$.

Imandra statement

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

Back to list

60. Bezout's Theorem

Source: src/gcd.iml

Statement (informal):

For all $a,b\in\mathbb{Z}$ there exist $x,y\in\mathbb{Z}$ such that $ax+by=\gcd(a,b)$.

In Imandra, we construct the Bezout coefficients with the function bezout_sub.

Imandra statement

let rec bezout_sub (a:int) (b:int) : int * int =
  if a < 0 || b < 0 then (0,0)
  else if a = 0 then (0,1)
  else if b = 0 then (1,0)
  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

Back to list

65. Isosceles Triangle Theorem

Source: src/isosceles.iml

Statement (informal):

In triangle $ABC$, if the two sides meeting at vertex $C$ are equal in length, i.e., $|AC| = |BC|$, then the base angles at $A$ and $B$ are equal:

$$\angle CAB = \angle ABC.$$

Imandra statement

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)

Back to list

69. Greatest Common Divisor Algorithm

Source: src/gcd.iml

Statement (informal):

For natural numbers $a,b$, the Euclidean GCD algorithm defined by repeated subtraction always terminates and yields a positive integer $g$ such that $g$ divides both $a$ and $b$, and every common divisor of $a$ and $b$ divides $g$.

Imandra statement

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)

theorem gcd_remainder_step a b =
  a >= 0 && b > 0 ==> gcd a b = gcd b (a mod b)

theorem gcd_dvd_both_pos a b =
  gcd a b > 0 ==> a mod (gcd a b) = 0 && b mod (gcd a b) = 0

theorem gcd_absorbs_common_divisor d a b =
  d > 0 && a mod d = 0 && b mod d = 0 ==> (gcd a b) mod d = 0

Back to list

74. Principle of Mathematical Induction

Source: src/math_induct.iml

Statement (informal):

If $P(0)$ holds and $\forall n,(P(n)\Rightarrow P(n+1))$, then $\forall n\in\mathbb{N},P(n)$.

Imandra statement

axiom base prop =
  prop 0

axiom inductive prop n =
  n >= 0 && prop n ==> prop (n+1)

theorem induction prop n =
  n >= 0 ==> prop n

Back to list

80. The Fundamental Theorem of Arithmetic

Source: src/fta.iml

Statement (informal):

Every integer $n>1$ can be expressed as a unique product of primes.

Imandra statement

theorem prime_factorization_exists n =
  n >= 2 
  ==> all_prime (prime_factors n) && prod_list (prime_factors n) = n

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

Back to list

85. Divisibility by 3 Rule

Source: src/div_by_3.iml

Statement (informal):

An integer $n$ is divisible by $3$ iff the sum of its base-$10$ digits is divisible by $3$.

Imandra statement

theorem sum_digits_preserves_mod3 n =
  n >= 0 ==> n mod 3 = sum_digits n mod 3

Back to list

91. The Triangle Inequality

Source: src/tri_ineq.iml

Statement (informal):

For all vectors $x, y$ in the plane, the length of their sum is at most the sum of their lengths:

$$|x + y| \le |x| + |y|.$$

Imandra statement

theorem triangle_inequality (x:R2.vec) (y:R2.vec) (nx:real) (ny:real) (nxy:real) =
  let open Real in
  let open R2 in
  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

Back to list

Contact

Grant Passmore ([email protected])