The Second 100

A Sequel to Freek100 (Draft)

A sequel to Freek Wiedijk's Formalizing 100 Theorems (Freek100): 100 theorems chosen by deliberation among Gemini, Claude and Codex, with an outside opinion from ChatGPT. Gemini proposed the first lists, Claude curated them into this one, and Codex reviewed it for overlaps, gaps and imprecise statements. We avoided repeating any of the original 100, although some of ours are generalizations or applications of them. The list is spread over sixteen areas and favors theorems that are foundational, surprising, or both. We also chose theorems that can be built into a readable book: the claim is clear, the assumptions can be stated, and the proof can be followed. Appearing here does not mean the theorem has been formalized. This is a draft; the points that are still open are listed at the end of the page.

Difficulty is the difficulty of the proof once the standard prerequisites are available: ★ = a short construction, a computation or one main idea; ★★ = several lemmas or stages, an ordinary university-textbook proof; ★★★ = a long construction, a classification or an intricate argument remains even with the prerequisites. The amount of preparation needed is not rated yet. Tags: foundational = much later mathematics rests on it; surprising = the statement is unexpected; major = a big theorem. Where the exact statement has been fixed, it is written under the title.

One more fact, found after the list was made: Freek Wiedijk's page records 41 theorems that people told him were missing from his list (checked on 10 November 2026). Fourteen of them are in this list: Borsuk–Ulam, Cauchy's integral theorem, the residue theorem, Gödel's completeness theorem, the fundamental theorem of finite abelian groups (we state the finitely generated case), the fundamental theorem of Galois theory, Heine–Borel, Hilbert's basis theorem, the Nullstellensatz, the Jordan curve theorem, the Riemann mapping theorem, Stone–Weierstrass, Banach–Tarski and the Yoneda lemma. Most of the others are research-level results, such as the classification of finite simple groups, the Feit–Thompson theorem and the Kepler conjecture. We did not choose theorems by this list; we only noticed the overlap afterwards.

The 100 Theorems

Number Theory (9)

1. Chinese Remainder Theorem ★ · foundational
   For pairwise coprime integers \(m_1,\ldots,m_r\ge2\), every system \(x\equiv a_i\pmod{m_i}\) has a unique solution modulo \(m_1\cdots m_r\).
2. Existence of Primitive Roots Modulo a Prime ★★ · foundational
3. Hensel's Lemma ★
   Let \(p\) be prime and \(f\in\mathbb Z_p[x]\); if \(a\in\mathbb Z_p\) satisfies \(f(a)\equiv0\pmod p\) and \(f'(a)\not\equiv0\pmod p\), then there is a unique \(\alpha\in\mathbb Z_p\) with \(f(\alpha)=0\) and \(\alpha\equiv a\pmod p\).
4. Lucas's Theorem (Binomial Coefficients Mod p) ★ · surprising
5. Legendre's Formula (Prime Powers Dividing n!) ★
6. Zeckendorf's Theorem ★ · surprising
   Every positive integer has a unique representation as a sum of distinct, nonconsecutive terms of the Fibonacci sequence \(F_1=1,\ F_2=2,\ F_{n+2}=F_{n+1}+F_n\).
7. The Frobenius Coin Problem (ab − a − b) ★ · surprising
   For coprime integers \(a,b>1\), the largest integer not expressible as \(ax+by\) with \(x,y\in\mathbb Z_{\ge0}\) is \(ab-a-b\).
8. Dirichlet's Approximation Theorem ★
   For every \(\alpha\in\mathbb R\) and integer \(Q\ge1\), there exist \(p\in\mathbb Z\) and \(1\le q\le Q\) such that \(|\alpha-p/q|<1/(qQ)\).
9. Euler Product for the Zeta Function ★★ · foundational
   For every complex \(s\) with \(\operatorname{Re}s>1\), the series and product in \(\zeta(s)=\sum_{n=1}^{\infty}n^{-s}=\prod_{p\ {\rm prime}}(1-p^{-s})^{-1}\) converge absolutely.

Algebra (15)

10. First Isomorphism Theorem for Groups ★ · foundational
11. Schur's Lemma ★ · foundational
    Every nonzero homomorphism between simple modules over a ring is an isomorphism, and every endomorphism of a finite-dimensional irreducible representation over an algebraically closed field is scalar.
12. Cayley's Theorem ★ · foundational
13. Burnside's Lemma ★
14. Fundamental Theorem of Finitely Generated Abelian Groups ★★★ · foundational
15. Wedderburn's Little Theorem (Finite Division Rings are Commutative) ★★ · surprising
16. Existence and Uniqueness of Finite Fields ★★ · foundational
    Every finite field has prime-power order, and for every prime \(p\) and integer \(n\ge1\) there exists, up to isomorphism, exactly one field with \(p^n\) elements.
17. Every PID is a UFD ★★ · foundational
18. Lagrange Interpolation ★
    Given pairwise distinct \(x_0,\ldots,x_n\) in a field \(F\) and arbitrary \(y_0,\ldots,y_n\in F\), there is a unique polynomial \(p\in F[x]\) of degree at most \(n\) satisfying \(p(x_i)=y_i\) for every \(i\).
19. Eisenstein's Irreducibility Criterion ★
20. The Tower Law for Field Extensions ★ · foundational
21. Hilbert's Basis Theorem ★★ · foundational
22. Hilbert's Nullstellensatz ★★★ · major
    For an algebraically closed field \(k\) and every ideal \(I\subseteq k[x_1,\ldots,x_n]\), the ideal of polynomials vanishing on \(V(I)\subseteq k^n\) is \(\sqrt I\).
23. Fundamental Theorem of Galois Theory ★★★ · major
    For a finite Galois extension \(L/K\), the maps \(E\mapsto\operatorname{Gal}(L/E)\) and \(H\mapsto L^H\) are inverse inclusion-reversing bijections, with \([L:E]=|\operatorname{Gal}(L/E)|\), and \(E/K\) is Galois exactly when \(\operatorname{Gal}(L/E)\) is normal, in which case its quotient is \(\operatorname{Gal}(E/K)\).
24. Maschke's Theorem (Group Algebras Are Semisimple When the Characteristic Does Not Divide the Group Order) ★ · foundational

Linear Algebra (7)

25. Rank–Nullity Theorem ★ · foundational
26. Steinitz Exchange Lemma and Uniqueness of Dimension (Finite-Dimensional Case) ★ · foundational
27. Multiplicativity of the Determinant ★ · foundational
28. Spectral Theorem for Real Symmetric Matrices ★★ · foundational
29. Existence of the Singular Value Decomposition ★
30. Jordan Normal Form ★★★ · major
    Every square matrix over an algebraically closed field is similar to a Jordan matrix whose blocks are uniquely determined up to permutation.
31. Perron–Frobenius Theorem (Positive Matrices) ★★
    Every real square matrix with strictly positive entries has a positive eigenvalue equal to its spectral radius, this eigenvalue is algebraically simple and has a strictly positive eigenvector, and every other eigenvalue has strictly smaller modulus.

Analysis (15)

32. Bolzano–Weierstrass Theorem ★ · foundational
33. Heine–Borel Theorem ★ · foundational
34. Banach Fixed-Point Theorem ★ · foundational
35. Picard–Lindelöf Theorem ★★
    If \(f:U\subseteq\mathbb R\times\mathbb R^d\to\mathbb R^d\) is continuous and locally Lipschitz in its second variable uniformly on a neighborhood of \((t_0,x_0)\in U\), then \(x'=f(t,x),\ x(t_0)=x_0\) has a unique local solution.
36. Inverse Function Theorem ★★
    If \(f:U\subseteq\mathbb R^n\to\mathbb R^n\) is \(C^1\) on an open set and \(Df(a)\) is invertible, then \(f\) restricts to a \(C^1\) diffeomorphism between neighborhoods of \(a\) and \(f(a)\).
37. Stone–Weierstrass Theorem ★★
    If \(X\) is compact Hausdorff and a real subalgebra \(A\subseteq C(X,\mathbb R)\) contains the constants and separates points, then \(A\) is dense in \(C(X,\mathbb R)\) in the uniform norm.
38. Arzelà–Ascoli Theorem ★★
    For a compact metric space \(K\), a family \(\mathcal F\subseteq C(K,\mathbb R)\) has compact closure in the uniform norm if and only if it is uniformly bounded and equicontinuous.
39. Baire Category Theorem ★ · foundational
    In every complete metric space, the intersection of countably many open dense subsets is dense.
40. Jensen's Inequality ★ · foundational
    If \(\varphi:I\to\mathbb R\) is convex on an interval, \(x_1,\ldots,x_n\in I\), and \(\lambda_i\ge0\) with \(\sum_i\lambda_i=1\), then \(\varphi(\sum_i\lambda_i x_i)\le\sum_i\lambda_i\varphi(x_i)\).
41. Hölder's Inequality ★ · foundational
    For \(1<p,q<\infty\) with \(1/p+1/q=1\) and finite real or complex sequences \((a_i),(b_i)\), \(\sum_i|a_i b_i|\le(\sum_i|a_i|^p)^{1/p}(\sum_i|b_i|^q)^{1/q}\).
42. Lebesgue's Dominated Convergence Theorem ★ · foundational
    If measurable real or complex functions \(f_n\) converge almost everywhere to \(f\) and satisfy \(|f_n|\le g\) almost everywhere for some integrable \(g\ge0\), then \(f\) is integrable and \(\int|f_n-f|\to0\).
43. Fubini's Theorem ★★
    For two \(\sigma\)-finite measure spaces and an integrable real or complex function on their product, almost all sections are integrable and both iterated integrals equal the product integral.
44. Hahn–Banach Theorem ★★ · major
    If \(p:X\to\mathbb R\) is sublinear on a real vector space and a linear functional \(f\) on a subspace satisfies \(f\le p\), then \(f\) extends to a linear functional \(F:X\to\mathbb R\) satisfying \(F\le p\).
45. Banach–Steinhaus Theorem (Uniform Boundedness Principle) ★ · foundational
    If \(X\) is a Banach space, \(Y\) is a normed space, and a family \(\mathcal T\) of bounded linear maps \(X\to Y\) satisfies \(\sup_{T\in\mathcal T}\|Tx\|<\infty\) for every \(x\in X\), then \(\sup_{T\in\mathcal T}\|T\|<\infty\).
46. Gabriel's Horn (Finite Volume, Infinite Surface Area) ★ · surprising
    The solid obtained by revolving the region \(x\ge1,\ 0\le y\le1/x\) about the \(x\)-axis has volume \(\pi\), while its lateral surface has infinite area.

Complex Analysis (4)

47. Cauchy's Integral Theorem and Integral Formula ★★ · foundational
    If \(f\) is holomorphic on a simply connected domain \(D\subseteq\mathbb C\), then \(\int_\gamma f(z)\,dz=0\) for every closed piecewise \(C^1\) curve \(\gamma\subset D\), and \(f(a)=\frac1{2\pi i}\int_C f(z)/(z-a)\,dz\) for every positively oriented circle \(C\) whose closed disk lies in \(D\) and whose interior contains \(a\).
48. Identity Theorem ★
49. Residue Theorem (with Applications to Real Integrals) ★★ · surprising
50. Riemann Mapping Theorem ★★★ · major
    Every nonempty simply connected proper domain in \(\mathbb C\) is biholomorphic to the open unit disk.

Topology (6)

51. Tychonoff's Theorem ★★ · major
    Assuming the axiom of choice, every set-indexed product of compact topological spaces is compact in the product topology.
52. Urysohn's Lemma ★★
    If \(X\) is a normal \(T_1\) space and \(A,B\subseteq X\) are disjoint closed sets, then there exists a continuous \(f:X\to[0,1]\) with \(f|_A=0\) and \(f|_B=1\).
53. The Fundamental Group of the Circle is Z ★★
54. Borsuk–Ulam Theorem ★★★ · surprising
55. Hairy Ball Theorem (Even-Dimensional Spheres) ★ · surprising
    Every continuous tangent vector field on an even-dimensional sphere \(S^{2k}\) vanishes at some point.
56. Jordan Curve Theorem ★★★ · major
    The complement in \(\mathbb R^2\) of the image of any continuous injection \(S^1\to\mathbb R^2\) has exactly two connected components, one bounded and one unbounded, and that image is the boundary of each component.

Discrete Mathematics (11)

57. Cayley's Formula (nⁿ⁻² Labeled Trees) ★★ · surprising
58. Hall's Marriage Theorem ★★ · foundational
59. König's Theorem (Bipartite Matching = Vertex Cover) ★★
60. Max-Flow Min-Cut Theorem ★★ · foundational
    In every finite directed network with distinct source and sink and finite nonnegative real capacities, the maximum value of a feasible flow equals the minimum capacity of a source–sink cut.
61. Turán's Theorem ★★ · foundational
62. Sperner's Theorem (Largest Antichain) ★ · surprising
63. Erdős–Ko–Rado Theorem ★★
    If \(n\ge2r\ge2\), every pairwise-intersecting family of \(r\)-element subsets of an \(n\)-element set has at most \(\binom{n-1}{r-1}\) members.
64. Kuratowski's Theorem (Planar Graphs) ★★★ · major
    A finite simple graph is planar if and only if it contains no subgraph that is a subdivision of \(K_5\) or \(K_{3,3}\).
65. Sprague–Grundy Theorem (Finite Impartial Games) ★★ · surprising
    For finite impartial games under normal play, the Sprague–Grundy value of a disjunctive sum is the bitwise xor of the component values, and a position is losing exactly when its value is zero.
66. Gale–Shapley Stable Marriage Theorem ★ · surprising
    For two finite sets of equal size whose members have strict complete preferences over the opposite set, the deferred-acceptance algorithm terminates with a stable perfect matching.
67. Pigeonhole Principle ★ · foundational
    If \(A\) and \(B\) are finite sets with \(|A|>|B|\), then no map \(A\to B\) is injective.

Logic and Computation (9)

68. Gödel's Completeness Theorem ★★★ · major
    For every set \(\Gamma\) of sentences and every sentence \(\varphi\) in a classical first-order language, \(\Gamma\models\varphi\) implies \(\Gamma\vdash\varphi\) in a fixed standard first-order proof calculus.
69. Compactness Theorem ★ · foundational
    A set of sentences in a classical first-order language has a model if and only if every finite subset has a model.
70. Löwenheim–Skolem Theorem ★★
    Every infinite structure in a countable first-order language has a countably infinite elementary substructure containing any prescribed countable subset of its domain.
71. Undecidability of the Halting Problem ★ · foundational
72. Rice's Theorem ★
73. Cook–Levin Theorem ★★★ · major
74. Church–Rosser Theorem (Lambda Calculus) ★★
    If an untyped lambda term \(M\) beta-reduces in zero or more steps to both \(N_1\) and \(N_2\), then some term \(P\) is reachable by beta-reduction from both \(N_1\) and \(N_2\), with terms identified up to alpha-equivalence.
75. Tarski's Undefinability of Truth ★★
    The set of Gödel numbers of first-order arithmetic sentences true in the standard structure \((\mathbb N,0,1,+,\times,<)\) is not definable in that structure by an arithmetic formula.
76. Knaster–Tarski Fixed-Point Theorem ★ · foundational
    For every monotone self-map of a complete lattice, its fixed points form a complete lattice under the inherited order.

Sets and Orders (5)

77. Zorn's Lemma (Equivalent to the Axiom of Choice and Well-Ordering) ★★ · foundational
    Over ZF, the axiom of choice, the well-ordering theorem, and the assertion that every partially ordered set in which every chain has an upper bound has a maximal element are equivalent.
78. König's Lemma ★
79. The Banach–Tarski Paradox ★★★ · surprising
    Assuming the axiom of choice, a solid ball in \(\mathbb R^3\) can be partitioned into finitely many subsets that can be moved by Euclidean isometries to form two disjoint solid balls congruent to the original.
80. A Countable Dense Linear Order Without Endpoints is Isomorphic to Q (Back-and-Forth) ★ · surprising
    Every countably infinite dense linear order without endpoints is order-isomorphic to \((\mathbb Q,<)\).
81. Russell's Paradox and the Nonexistence of a Universal Set ★ · foundational
    No set \(R\) satisfies \(\forall x\,(x\in R\leftrightarrow x\notin x)\), and the separation schema therefore rules out a set containing every set.

Probability (5)

82. Markov's and Chebyshev's Inequalities ★ · foundational
83. Borel–Cantelli Lemma ★ · foundational
    For events \(A_n\), \(\sum_n\mathbb P(A_n)<\infty\) implies \(\mathbb P(A_n\text{ infinitely often})=0\), while independence and \(\sum_n\mathbb P(A_n)=\infty\) imply that this probability is \(1\).
84. The Probabilistic Method: R(k,k) > 2^(k/2) for k ≥ 3 ★ · surprising
85. Pólya's Recurrence Theorem (Random Walks on Zᵈ) ★★★ · surprising
    Simple symmetric nearest-neighbor random walk on \(\mathbb Z^d\) is recurrent for \(d=1,2\) and transient for every \(d\ge3\).
86. Gambler's Ruin ★
    For simple symmetric random walk started at \(i\in\{1,\ldots,N-1\}\) and stopped on first reaching \(0\) or \(N\), the probability of reaching \(N\) is \(i/N\) and the expected stopping time is \(i(N-i)\).

Elementary and Convex Geometry (7)

87. The Euler Line (Orthocenter, Centroid and Circumcenter are Collinear) ★
    In every nondegenerate Euclidean triangle, the circumcenter \(O\), centroid \(G\), and orthocenter \(H\) satisfy \(\overrightarrow{OG}=\frac13\overrightarrow{OH}\), and hence are collinear.
88. Sylvester–Gallai Theorem ★ · surprising
89. Menelaus's Theorem ★
90. Pappus's Hexagon Theorem ★
    For three distinct points \(A,B,C\) on one line and three distinct points \(A',B',C'\) on another line in the real projective plane, none at the intersection of the two lines, the points \(AB'\cap A'B\), \(AC'\cap A'C\), and \(BC'\cap B'C\) are collinear.
91. Napoleon's Theorem ★ · surprising
92. Gauss–Wantzel Theorem (Constructible Regular Polygons) ★★★ · major
    A regular \(n\)-gon, \(n\ge3\), is constructible with straightedge and compass if and only if \(n=2^a p_1\cdots p_r\), where \(a\ge0\) and the \(p_i\) are distinct Fermat primes.
93. Helly's Theorem ★★ · surprising
    If every subfamily of at most \(d+1\) members of a finite family of convex subsets of \(\mathbb R^d\) has nonempty intersection, then the entire family has nonempty intersection.

Category Theory (2)

94. Yoneda Lemma ★ · foundational
    For a locally small category \(\mathcal C\), an object \(A\), and a functor \(F:\mathcal C\to\mathbf{Set}\), evaluation at \(1_A\) gives a bijection \(\operatorname{Nat}(\mathcal C(A,-),F)\cong F(A)\), natural in \(A\) and \(F\).
95. Right Adjoints Preserve Limits ★
    If \(R:\mathcal D\to\mathcal C\) is a right adjoint and a small diagram \(D:J\to\mathcal D\) has a limit cone, then applying \(R\) to that cone gives a limit cone for \(R\circ D\).

Social Choice and Games (2)

96. Arrow's Impossibility Theorem (Three or More Alternatives) ★★ · surprising
    For a finite electorate of at least two voters and a finite set of at least three alternatives, every rule assigning a social linear order to every profile of individual linear orders and satisfying Pareto unanimity and independence of irrelevant alternatives is dictatorial.
97. Existence of Nash Equilibrium (Mixed Strategies, Finite Games) ★★
    Every finite game with a nonempty finite strategy set for each player and real-valued payoffs has a mixed-strategy Nash equilibrium.

Information Theory (1)

98. Shannon's Source Coding Theorem (Average Code Length for a Finite Memoryless Source) ★★ · foundational
    For an i.i.d. source \(X\) on a finite alphabet of at least two symbols with positive probabilities, the minimum expected length \(L_n^*\) of a binary prefix code for blocks of \(n\) symbols satisfies \(H(X)\le L_n^*/n<H(X)+1/n\), with entropy measured in bits.

Dynamical Systems (1)

99. Poincaré Recurrence Theorem (Finite Measure-Preserving Systems) ★ · surprising
    If \(T\) is a measurable measure-preserving self-map of a finite measure space, then for every measurable set \(A\), almost every \(x\in A\) satisfies \(T^n(x)\in A\) for infinitely many positive integers \(n\).

Differential Geometry (1)

100. Gauss–Bonnet Theorem (Closed Orientable Surfaces) ★★★ · major
     For every smooth compact oriented two-dimensional Riemannian manifold \(M\) without boundary, \(\int_M K\,dA=2\pi\chi(M)\), where \(K\) is the Gaussian curvature.

The following problems are also candidates

These are proposals that are not among the 100 above. They were left out to avoid overlap, to balance the areas, or because they are too heavy, or they were replaced in the final round. They remain as possible replacements.

Algebra

• First Isomorphism Theorem for rings, \(R/\ker\psi \cong \mathrm{Im}\,\psi\)
• Maximal ideals and quotient fields (\(R/I\) is a field \(\iff I\) is maximal); prime ideals and integral domains
• Universal property of free modules
• Structure theorem for finitely generated torsion modules over a PID
• Noether normalization
• Krull's prime avoidance lemma
• Nakayama's lemma
• Simplicity of the alternating group Aₙ (n ≥ 5)
• Frobenius reciprocity
• Isomorphism theorems for groups and the subgroup correspondence
• Gauss's lemma and unique factorization in Z[x]

Linear Algebra

• Existence of a basis (finite-dimensional case)
• Linear maps and matrices: \(\mathcal{L}(V,W) \cong M_{m\times n}(F)\)
• Equivalent conditions for a square matrix to be invertible
• Gram–Schmidt orthogonalization
• Uniqueness of the Moore–Penrose pseudoinverse

Topology and Analysis

• Universal properties of the subspace, product and quotient topologies
• Uniqueness of limits in Hausdorff spaces
• Closed subsets of compact spaces are compact
• The continuous image of a connected space is connected
• Open mapping theorem and closed graph theorem
• Riesz–Markov–Kakutani representation theorem
• Radon–Nikodym theorem
• Sobolev embedding theorem (the one-dimensional case)
• Carathéodory's extension theorem
• Birkhoff's pointwise ergodic theorem
• Poincaré–Bendixson theorem
• Generalized Stokes theorem, \(\int_{\partial M}\omega=\int_M d\omega\)
• Liouville's theorem in complex analysis (a bounded entire function is constant)
• Rouché's theorem
• Bohr–Mollerup theorem (characterization of the Gamma function)
• A continuous bijection from a compact space to a Hausdorff space is a homeomorphism

Geometry, Manifolds and Algebraic Topology

• de Rham theorem (low-dimensional case)
• Seifert–van Kampen theorem
• Poincaré–Hopf index theorem
• Hopf–Rinow theorem
• The snake lemma
• Mayer–Vietoris sequence
• The five lemma
• Smale's sphere eversion
• The nine-point circle
• Erdős–Mordell inequality

Logic, Computation and Category Theory

• Curry–Howard correspondence (simply typed lambda calculus and intuitionistic propositional logic)
• Kleene's recursion theorems
• Scott continuity and the Kleene fixed-point theorem
• Herbrand's theorem
• Birkhoff's HSP theorem
• Goodstein's theorem
• κ·κ = κ for infinite well-orderable cardinals (in ZF)

Discrete Mathematics

• Menger's theorem
• Lovász local lemma
• Gilmer's theorem (a union-closed family has an element in a constant fraction of its sets)
• Golomb rulers from difference sets (Singer's construction)
• The Monty Hall problem and Bayes' theorem
• Dilworth's theorem

Short basic theorems (proposed to widen the range)

• Handshake lemma (the degrees sum to twice the number of edges)
• Bernoulli's inequality
• Archimedean property of the real numbers
• Brahmagupta–Fibonacci identity (products of sums of two squares)

Numbers, Dynamics and Information

• Apéry's theorem (\(\zeta(3)\) is irrational)
• Sharkovskii's theorem (the full ordering of periods; period 3 implies every period)
• Shannon's noisy-channel coding theorem
• von Neumann's minimax theorem

Decisions and open points

Gemini, Claude, Codex and ChatGPT did not always agree. Here is what we decided on 10 November, who disagreed, and what is still open.

Decided

• Six swaps were made: group isomorphism theorems → Schur's lemma; Gauss's lemma → Banach–Steinhaus; Bohr–Mollerup → Gabriel's horn; Dilworth → Gauss–Bonnet; κ·κ = κ → pigeonhole principle; Erdős–Mordell → Lagrange interpolation. With the six earlier swaps, twelve theorems have been replaced since the first draft. The hairy ball theorem was swapped out and then put back after a vote.
• The last three contested swaps (the hairy ball theorem, Gabriel's horn and Gauss–Bonnet) were settled by a vote: Codex, ChatGPT, Claude and the editor each scored every swap from −2 to +2. The hairy ball theorem was put back; the other two swaps stay.
• Kept: Kuratowski, Banach–Tarski, Church–Rosser and the Jordan curve theorem. Gemini and ChatGPT wanted these famous theorems to stay, and Codex agreed in the final round.
• Not adopted: the handshake lemma, Bernoulli's inequality and the Brahmagupta–Fibonacci identity (they stay in the candidates). Euler's polyhedron formula and the Four Color Theorem were proposed, but they are Freek100 #13 and #32. The Monty Hall problem stays a candidate.
• Stars now follow one rule (see the top of the page). This lowered many stars: there are now far more one-star theorems than before. The change comes from the new rule, not from any change in the work needed to formalize them.

Dissent and doubts

• The hairy ball theorem was first swapped for a short topological lemma (a continuous bijection from a compact to a Hausdorff space), then restored after a vote among the reviewers and the editor, because readers remember it. The short lemma moved to the candidates.
• ChatGPT hesitated about Gauss–Bonnet, which is heavy (three stars). It was kept because it opens differential geometry. It may be the first thing we reverse.
• Bohr–Mollerup and Dilworth were good theorems. Losing them is the price of the swaps.
• Gabriel's horn is a calculus computation rather than a deep theorem, and it may be called too light. We chose it for the surprise.
• Partial dependence on Freek100 remains: Hölder and Cauchy–Schwarz, Pappus and Pascal, dominated convergence, Fubini and Lebesgue integration.

Still open

• Preparation needed: should theorems that need a lot of prior theory carry a separate mark (for example †)? Codex suggested it. We have not assigned any marks yet.
• The exact statements are fixed for about sixty theorems. The rest still need a one-sentence statement.
• Differential geometry has one theorem now; partial differential equations, numerical analysis, optimization and the computation tools of algebraic topology are still thin.
• The Second 100 is a working name for this page. Scoring (proof length and speed) comes after the list is final.