The ImandraX 100 Theorems Project
The Top 100 Mathematical Theorems list, compiled by Paul Sally and popularized by Freek Wiedijk, is a benchmark for formal proof systems. It includes foundational results from number theory, algebra, geometry, analysis, and combinatorics.
ImandraX is not just an environment for reasoning about programs — it is also a powerful interactive theorem prover for formalizing mathematics, with unique strengths due to its computational logic and industrial-strength proof and counterexample automation. The ImandraX 100 Theorems project is an ongoing effort by Grant Passmore to formalize these theorems in ImandraX, demonstrating the system's mathematical reasoning capabilities.
Status: 20 / 100
Progress
20 of the 100 theorems have been formally proved in ImandraX. The project is ongoing — contributions welcome!
Proved theorems
| # | Theorem | Source |
|---|---|---|
| 1 | Irrationality of √2 | sqrt2_irrational.iml |
| 3 | Denumerability of the Rationals | q_denum.iml |
| 4 | Pythagorean Theorem | pythagoras.iml |
| 11 | Infinitude of Primes | inf_primes.iml |
| 34 | Divergence of the Harmonic Series | harmonic.iml |
| 42 | Sum of Reciprocals of Triangular Numbers | triangular.iml |
| 44 | Binomial Theorem | binomial.iml |
| 52 | Number of Subsets of a Set | num_subsets.iml |
| 54 | Konigsberg Bridges Problem | konigsberg.iml |
| 58 | Formula for Number of Combinations | combinations.iml |
| 60 | Bezout's Theorem | gcd.iml |
| 65 | Isosceles Triangle Theorem | isosceles.iml |
| 66 | Sum of a Geometric Series | geometric_series.iml |
| 68 | Sum of an Arithmetic Series | arithmetic_series.iml |
| 69 | Greatest Common Divisor Algorithm | gcd.iml |
| 74 | Principle of Mathematical Induction | math_induct.iml |
| 78 | Cauchy-Schwarz Inequality | cauchy_schwarz.iml |
| 80 | Fundamental Theorem of Arithmetic | fta.iml |
| 85 | Divisibility by 3 Rule | div_by_3.iml |
| 91 | Triangle Inequality | tri_ineq.iml |
Spotlight: Irrationality of √2
The proof that √2 is irrational is one of the most celebrated results in mathematics. The ImandraX formalization follows a proof by infinite descent:
- Assume √2 = p/q where p/q is in reduced form (gcd(p,q) = 1)
- Then p² = 2q²
- Therefore p² is even, so p is even (proved via modular arithmetic)
- Write p = 2k, then 4k² = 2q², so q² = 2k², and q is even
- But then both p and q are even, contradicting gcd(p,q) = 1
The formalization involves substantial development of modular arithmetic (mod properties), GCD theory, and careful reasoning about squares and parity. Key theorems include:
(* Squares preserve parity *)
theorem square_even_iff_even x =
((x * x) mod 2 = 0) = (x mod 2 = 0)
(* GCD absorbs common divisors *)
theorem gcd_absorbs_common_divisor d p q =
(d > 0 && p mod d = 0 && q mod d = 0)
==> (gcd p q) mod d = 0
(* No coprime solution to p² = 2q² *)
theorem no_coprime_solution_p2_eq_2q2 p q =
(gcd p q = 1 && p * p = 2 * (q * q))
==> false
(* The main result *)
theorem sqrt2_is_irrational (r : Rational.t) =
Rational.is_reduced r
==> Rational.square r <> Rational.of_int 2The full proof is approximately 200 lines of IML, including the modular arithmetic library and GCD theory. It demonstrates ImandraX's ability to handle deep, multi-step mathematical proofs with sophisticated tactic composition.
Mathematical areas covered
The proved theorems span a range of mathematical disciplines:
- Number theory: Irrationality of √2 (#1), infinitude of primes (#11), Bezout's theorem (#60), GCD algorithm (#69), fundamental theorem of arithmetic (#80), divisibility by 3 (#85)
- Algebra: Binomial theorem (#44), Cauchy-Schwarz inequality (#78)
- Analysis: Divergence of harmonic series (#34), geometric series (#66), arithmetic series (#68)
- Combinatorics: Number of subsets (#52), combinations formula (#58)
- Geometry: Pythagorean theorem (#4), isosceles triangle (#65), triangle inequality (#91)
- Set theory / logic: Denumerability of rationals (#3), mathematical induction (#74)
- Graph theory: Konigsberg bridges (#54)
How to explore the proofs
- Clone the repository:
git clone https://github.com/imandra-ai/imandra-100-theorems - Open any
.imlfile in VS Code with the ImandraX extension - Use the goal state viewer to step through the proofs interactively
- Try modifying proofs or proving the remaining 80 theorems!