My 100 theorems

I have compiled this list of 100 new theorems to prove using mathlib4. Some of these (like the Feit–Thompson theorem) have already been proved in other proof assistants, but that is largely irrelevant here; I have tried to ensure that no theorem from Freek's original list of 100 is in here and that there is a focus on more recent mathematics.

Disclaimer: No attempt has been made, though, to make the theorems of high importance – Freek's list already captures most of the important ones, and a few of the theorems are based off my own research on the Mathematics Stack Exchange.

If there are duplicates with the original list or any theorem is already within mathlib4 please let me know.

Analysis

1. PROVED Correctness of John Machin's original formula for $\pi$.
   $$\frac\pi4=4\arctan\frac15-\arctan\frac1{239}$$
2. Legendre's relation of complete elliptic integrals. Let $K$ and $E$ be the complete elliptic integrals of the first and second kinds respectively. Then
   $$K(m)E(1-m)+K(1-m)E(m)-K(m)K(1-m)=\frac\pi2$$
   where $m$ is the parameter.
3. Closed-form expression of the "continued fraction constant".
   $$[0;1,2,3,4,\dots]=\frac{I_1(2)}{I_0(2)}$$
4. Apéry's proof that $\zeta(3)$ is irrational.
5. Bourget's hypothesis. For distinct nonnegative integers $m,n$, the Bessel functions $J_m(x)$ and $J_n(x)$ only have at most one common zero, at $x=0$ (Siegel).
6. Frullani's integral. Let $a,b>0$ and $f$ be a continuously differentiable function on $\Bbb R_{\ge0}$ with a finite limit $f(\infty)$ at $\infty$. Then
   $$\int_0^\infty\frac{f(ax)-f(bx)}x dx=(f(\infty)-f(0))\ln\frac ab$$
7. de Branges's theorem aka Bieberbach conjecture. Let $f$ be a holomorphic function in the open unit disc with Taylor series $$z+\sum_{n=2}^\infty a_nz^n$$
   If $f$ is injective on the disc, $|a_n|\le n$ for all $n\ge2$.
8. Helmholtz decomposition. A twice-differentiable 3D vector field over a bounded domain can be decomposed into a curl-free part and a divergence-free part. If the domain is all space, this decomposition still exists if the field decays as fast as $1/r$.
9. The hypergeometric function at 1. If the real part of $c-a-b$ is positive,
   $${}_2F_1(a,b;c;1)=\frac{\Gamma(c)\Gamma(c-a-b)}{\Gamma(c-a)\Gamma(c-b)}$$
10. Riemann mapping theorem. For any two nonempty simply connected proper open subsets of the complex plane, there exists a biholomorphic map between them.
11. Perron–Frobenius theorem. A real square matrix with positive entries has a unique eigenvalue with largest magnitude; that eigenvalue is real and its corresponding eigenvector can be chosen to have positive entries only.
12. Cantor function. The Cantor function is continuous everywhere, monotone and differentiable almost everywhere but is not the integral of its derivative.

Combinatorics

13. Existence of some Steiner systems. (a) There exist Steiner triple systems for any number of items $\equiv1,3\bmod6$ (Skolem). (b) There exist Steiner quadruple systems for any number of items $\equiv2,4\bmod6$ (Hanani).
14. Conway's cosmological theorem. (a) All evolutions of the look-and-say sequence eventually decay into sequences of 92 "elements" (if only digits from 1 to 3 are used initially) where each element never again affects its neighbours. (b) The ratio between consecutive iterations of any look-and-say sequence except that starting from 22 approaches the degree-71 algebraic number called Conway's constant.
15. Conway's Soldiers is unsolvable in a finite number of moves when the target row is the fifth or beyond.
16. Zeilberger's alternating sign matrix theorem. The number of n × n alternating sign matrices is
    $$\prod_{k=0}^{n-1}\frac{(3k+1)!}{(n+k)!}$$
17. There exist pairs of orthogonal Latin squares for any order except 2 and 6.
18. Impossibility of a pentomino puzzle. It is impossible to use the 12 free pentominoes to tile the following shape:

     #
    ###
   #####
  #######
 #########
##### #####
 #########
  #######
   #####
    ###
     #

19. Crank of a partition. The crank as defined by Andrews and Garvan divides the partitions of $5n+4,7n+5,11n+6$ into $5,7,11$ equally sized classes based on the crank residue modulo $5,7,11$ respectively.
20. Number of de Bruijn sequences. Up to cyclic rotations, there are $(k!)^{k^{n-1}}/k^n$ distinct de Bruijn sequences for length $n$ words on a size $k$ alphabet.
21. Polyá's enumeration theorem.
22. Aztec diamonds. The number of domino tilings of the order $n$ Aztec diamond is $2^{n(n+1)/2}$.
23. Testing sorting networks. To validate a sorting network for $n$ items it suffices to test all $2^n$ inputs containing just zeros and ones.
24. Alternating permutations. The generating function for the number of permutations where successive pairs of elements alternately compare greater and lesser, with the first element less than the second, is $\sec x+\tan x$.
25. Chen–Fox–Lyndon theorem. Any word has a unique decomposition into a non-increasing sequence of Lyndon words.
26. Perfect codes. Over alphabets of prime-power size, any non-trivial perfect code is either a Hamming code or one of the two Golay codes (Tietäväinen 1973).
27. Even–Gillis formula for generalised derangements. Consider a deck where there are $s_i$ identical cards of rank $i$ for $1\le i\le n$. Then the number of derangements of this deck is, up to sign,
    $$\int_0^\infty e^{-x}\prod_{i=1}^nL_{s_i}(x)\,dx$$
    where $L$ denotes the Laguerre polynomials. In particular, there are exactly 1493804444499093354916284290188948031229880469556 ways to derange a standard deck of cards ignoring suits.
28. The game of Hex cannot end in a tie.
29. First paper in Discrete Analysis aka Erdős discrepancy problem. For any infinite sequence $\{x_i\}$ with only $\pm1$ and any positive integer $b$ there exist positive integers $n$ and $d$ such that the sum of terms $x_{kd}$ for $1\le k\le n$ has magnitude at least $b$.
30. Thue–Morse sequence along the squares. The binary sequence defined by the parity of the Hamming weight of $n^2$ (OEIS A228039) is normal, i.e. every binary word of length $k$ appears as a contiguous subsequence with frequency $1/2^k$ (Drmota, Mauduit, Rivat 2013).
31. Maximum overhang. The maximum overhang over the edge of a table acheivable by a 2D stack of $n$ ideal Jenga blocks is $\Theta(n^{1/3})$ (Paterson et al. 2007).
32. Pentagonal number recurrence for partitions. The unrestricted partition function $p(n)$ satisfies
    $$p(n)=\sum_{k\in\Bbb Z,k\ne0}(-1)^{k+1}p(n-k(3k-1)/2)$$

Geometry

33. There are exactly 92 Johnson solids.
34. Equivalence of the geometric and algebraic constructions of the isogonal conjugate. Consider a nondegenerate triangle ABC and a point P strictly inside it, with trilinear coordinates $x:y:z$. Reflect the cevian PA across the bisector of angle A, and similarly for PB and PC. Prove that the reflected cevians concur at a point with trilinear coordinates $1/x:1/y:1/z$.
35. The densest packing of 9 equal-sized circles in a square is the obvious one.
36. The Penrose rhombus tiles are aperiodic.
37. Correctness of Andrew M. Gleason's construction of a regular heptagon using one angle trisection – see here for an animation.
38. Banach–Tarski paradox, original form. In 3D or higher Euclidean space, any two bounded subsets of the space $A,B$ with nonempty interior can each be decomposed into some finite number of pieces $A_1,\dots,A_n$ and $B_1,\dots,B_n$ such that each $A_i$ - $B_i$ pair is a congruence.
39. Poncelet–Steiner theorem. The compass in any compass-and-straightedge construction can be replaced by a pre-drawn circle and its centre.
40. Theorema egregium. The Gaussian curvature of a surface is invariant under local isometries.
41. Willmore energy. The integral of squared mean curvature over a surface homeomorphic to a sphere is at least $4\pi$, with equality iff it actually is a sphere.
42. Marden's theorem. Place three points in the complex plane and form a triangle out of them as well as a cubic polynomial $p$ with the corresponding complex numbers as roots. The foci of the triangle's Steiner inellipse are the roots of $p'$.
43. Malfatti circles are never the optimal solution to the problem of maximising the area of three circles cut out of a triangle.

Graph theory

44. Brooks's theorem. Except for odd cycles and complete graphs, any graph with maximum vertex degree $\Delta$ can be coloured with $\Delta$ colours.
45. Generalised Vizing's theorem. For a multigraph with maximum multiplicity $\mu$ and maximum vertex degree $\Delta$, its edges can be properly coloured with at most $\Delta+\mu$ colours.
46. BEST theorem. In a directed graph, the number of Eulerian circuits can be computed in polynomial time by computing a determinant and multiplying it with some factorial factors.
47. "Double-delta theorem" on unit-distance graphs. Except for $K_{3,3}$, any connected graph with maximum vertex degree $\Delta$ can be embedded in $\mathbb R^\Delta$ nondegenerately so that all edges are of unit length (Frankl, Kupavskii, Swanepoel 2018).
48. Strong perfect graph theorem. A graph is perfect iff neither it or its complement contains an induced cycle of odd length 5 or more.
49. Graphs with specified Wiener index. Every positive integer except 2 and 5 is the Wiener index of some graph.
50. The only known nontrivial multipartite Ramsey number. $K_{17}$ is the smallest complete graph for which every 3-colouring of its edges has a monochromatic triangle.
51. Forbidden induced subgraph characterisation of line graphs. A graph is a line graph iff it contains none of the nine graphs shown here as an induced subgraph.
52. Steinitz's theorem on polyhedral graphs. The graphs that are skeletons of convex polyhedra are exactly the planar 3-vertex-connected graphs.
53. Existence of knight's tours. Closed knight's tours exist on all rectangular chessboards with an even number of squares except when the smaller dimension is 1, 2 or 4 or the board is 3 × {4, 6, 8}.
54. Frucht's theorem. Any finite group is the automorphism group of some finite 3-regular graph.
55. Ringel–Youngs theorem aka Heawood conjecture. A graph embeddable on a closed surface that is not the sphere and has Euler characteristic χ has chromatic number at most
    $$\left\lfloor\frac{7+\sqrt{49-24χ}}2\right\rfloor$$
    and this upper bound is tight except on the Klein bottle.
56. Robertson–Seymour theorem. Every minor-closed family of graphs is characterised by a finite set of forbidden minors.

Group theory and higher algebra

57. There are exactly 17 wallpaper groups.
58. Burnside's two-prime theorem. Every group whose order has only two distinct prime factors is solvable.
59. Feit–Thompson theorem. Every group of odd order is solvable.
60. Generalised crystallographic restriction theorem. Define an additive function $\psi(m)$ that equals the totient function for odd primes and their powers but is 0 at 1 and 2. Then if an n × n integer matrix has finite order m, $\psi(m)\le n$.
61. Hurwitz's theorem on composition algebras. The only normed division algebras over $\Bbb R$ are $\Bbb R,\Bbb C,\Bbb H,\Bbb O$.
62. Stufe. The Stufe of a field is the least number of squares needed to sum to -1, or $\infty$ if this is impossible. Prove that (a) if the Stufe is finite it is a power of 2 and (b) every power of 2 is the Stufe of some field.
63. Conway's sporadic groups. The quotient of the automorphism group of the Leech lattice by its centre is a simple group not of Lie type, as are the groups of automorphisms that fix a type 2 or type 3 vector.
64. Dual Circle. In Oskar van Deventer's Dual Circle puzzle, only $6^{11}$ positions can be reached rather than the $6^{12}$ that would be naively expected. (Jaap says that this "twist restriction is rather complicated, and not at all obvious".)

Knot theory and topology

65. The only knot with 4 crossings (up to isomorphism) is the figure-eight knot.
66. Classification of knots. Every knot is either torus, hyperbolic or satellite (Thurston).
67. The Conway knot is not a slice knot (Piccirillo 2020).
68. Hairy ball theorem. Any continuous tangential vector field on $\Bbb S^{2n}$ vanishes somewhere.
69. Ropelength. The ropelength of a nontrivial knot is at least 15.66 (Denne, Diao, Sullivan 2006).

Logic, computability and computational complexity

70. Goodstein's theorem. (a) Every Goodstein sequence terminates at 0. (b) This is not provable in Peano arithmetic.
71. Cook's theorem. The Boolean satisfiability problem is NP-complete.
72. The other Cook's theorem – universality of Wolfram's rule 110. The 1D "elementary cellular automaton" called rule 110 by Wolfram, given appropriate initial conditions, is Turing-complete for an appropriate notion of "Turing-complete".
73. Mortal matrix problem. Given two 15 × 15 matrices, it is undecidable whether the monoid generated by those matrices and matrix multiplication contains the zero matrix (Cassaigne et al. 2014).
74. The Schröder–Bernstein theorem implies excluded middle (Pradic & Brown 2019).
75. Optimality of a disjoint-set data structure implementation. (a) Using path compression/splitting/halving together with union-by-size/rank for a disjoint-set data structure makes the amortised running time per operation $\Theta(\alpha(n))$ if there are $n$ elements to start with, where $\alpha$ is the inverse Ackermann function. (b) This is asymptotically optimal (Fredman & Saks 1989).
76. Greibach normal form. For every context-free grammar (CFG) there is an equivalent CFG where all rules are of the form $A\to aBCD\dots$ where $a$ is a terminal and the other letters represent nonterminals.
77. Life is omniperiodic. For every positive integer there exists an oscillator in Conway's Game of Life with said integer as period.

Number theory

78. Mihăilescu's theorem aka Catalan conjecture. 8 and 9 are the only two consecutive nontrivial perfect powers.
79. Green–Tao theorem. There are arithmetic progressions of arbitrary length consisting only of prime integers.
80. Størmer's theorem. (a) There are finitely many pairs of consecutive numbers that are both smooth with respect to any fixed set of primes containing 2. (b) There is an explicit algorithm to find all such pairs.
81. A hyperelliptic equation associated with rationally bracing a regular nonagon. If in $y^2=1+6a+24a^2+48a^3+144a^4+288a^5+192a^6$ both $y,a$ are rational, $a\in\{-1/2,0,1/4,3/2\}$.
82. Helfgott's theorem aka ternary Goldbach conjecture. Every odd number at least 7 can be written as the sum of three primes.
83. Correctness and polynomial running time of the AKS primality test.
84. The smallest Pisot–Vijayaraghavan number is the plastic constant, the unique real root of $x^3-x-1$.
85. For any fixed decimal digit there are infinitely many primes not containing that digit in their decimal expansion (Maynard).
86. Irregularity of distributions. There is no sequence of 18 real numbers between 0 and 1 such that the first $i$ numbers lie in different $i$-ths for $1\le i\le18$.
87. Baker–Stark–Heegner theorem. There are exactly 9 positive integers for which $\Bbb Q[\sqrt{-d}]$ has unique factorisation (class number 1).
88. PROVED Cannonball problem. The only numbers that are both square and square pyramidal are $1^2$ and $70^2$.
89. Mazur's torsion theorem. Torsion groups of elliptic curves over the rationals can only be cyclic of orders 1 to 12 except 11, or $C_2$ times a cyclic group of orders 1 to 4.
90. PROVED Rayleigh theorem on Beatty sequences. Given the Beatty sequence associated with an irrational number $r>1$, the Beatty sequence associated to $r/(r-1)$ is complementary in the sense that every positive integer appears in exactly one of the two sequences.
91. "Interesting" numbers. Call a number interesting if it is a semiprime $pq$ with $p\ne q$ and $pq+1=(\text{previous prime before }p)(\text{next prime after }q)$. Show that 14 and 21 are the only interesting numbers.

Probability

92. Memorylessness. The only discrete/continuous memoryless probability distributions are the geometric/exponential distributions respectively.
93. Raikov's theorem. If the sum of two independent variables is Poisson-distributed, so are each of the two summand variables.
94. Triangle enclosing fixed point in circle. In the unit circle centred on the origin fix a point $(x,0)$ with $0\le x\le1$. Now choose three points uniformly at random on the circle's circumference. Show that the probability of the triangle formed by the random points enclosing the fixed point is
    $$\frac14-\frac3{2\pi^2}\mathrm{Li}_2(x^2)$$
    where the special function is the dilogarithm.
95. Extreme value theorem. Given a sample of iid random variables, if the random variable corresponding to the sample maximum converges in distribution (after suitable normalisation) as the sample size tends to infinity, the limit distribution is either a Fréchet, Gumbel or Weibull distribution.
96. Cramér–Rao bound. Under suitable regularity conditions, any unbiased estimator of the parameter of a one-parameter probability distribution has variance at least the reciprocal of the Fisher information.
97. Secretary problem. The optimal solution to the secretary problem consists of rejecting the first $x$ applicants and then selecting the first new one that is better than all seen so far, for $x$ depending on the applicant pool's size $n$; $\lim_{n\to\infty}x/n=1/e$.
98. Cycle-following for freedom. (a) The cycle-following scheme for the 100 prisoners problem has a success rate approaching $1-\ln2$ as the number of prisoners tends to infinity. (b) This scheme is optimal (Curtin, Warshauer 2006).

Miscellaneous

99. Sharkovskii's theorem. Consider a continuous function $f$ from a real interval to itself. (a) If $f$ has a period $2^n$ cycle it also has period $2^m$ cycles for $m\le n$. (b) If $f$ has a period $k\cdot 2^n$ cycle where $k$ is an odd number greater than 1, it also has periods of all powers of two and period $k'\cdot 2^{n'}$ cycles where $k'$ is an odd number and $n'>n$ or $n'=n$ and $k'>k$.
100. Hearing the shape of a drum. The two ideal drums constructed by Gordon, Webb and Wolpert in 1992 – seen here – have the same eigenspectrum.

The issue body is the only entry point and lists 100 proposed theorem formalizations, with some linked mathlib4 documentation. Start by narrowing the list to one theorem and checking whether it already exists; the issue needs a specific theorem, source location, and verification target before completion can be defined.