OmegaCombinator's Freek Top 100 Formalization Project in Acorn

Freek Wiedijk's list of one hundred mathematical theorems has long served as a compact way to understand the reach of a theorem-proving system. It is broad enough to touch much of ordinary mathematics, but concrete enough that progress can be measured theorem by theorem. A prover that makes progress on the list has to do more than manipulate syntax. It needs a library, a mathematical vocabulary, proof search, replayable proofs, and enough ergonomic surface area for people to keep building.

OmegaCombinator Lab, a China-based research organization and open community behind AI x Math, has been using this list as a public benchmark for Acorn. As of May 2026, our project has completed 29 verified entries out of 100. The results are tracked publicly at 100.aixmath.org, with the broader AI x Math portal at aixmath.org.

The completed entries currently are:

#	Theorem
1	The Irrationality of the Square Root of 2
3	The Denumerability of the Rational Numbers
4	Pythagorean Theorem
10	Euler's Generalization of Fermat's Little Theorem
11	The Infinitude of Primes
25	Schroeder-Bernstein Theorem
30	The Ballot Problem
34	Divergence of the Harmonic Series
42	Sum of the Reciprocals of the Triangular Numbers
44	The Binomial Theorem
51	Wilson's Theorem
52	The Number of Subsets of a Set
54	Konigsberg Bridges Problem
55	Product of Segments of Chords
57	Heron's Formula
58	Formula for the Number of Combinations
60	Bezout's Theorem
63	Cantor's Theorem
66	Sum of a Geometric Series
68	Sum of an Arithmetic Series
69	Greatest Common Divisor Algorithm
71	Order of a Subgroup
74	The Principle of Mathematical Induction
78	The Cauchy-Schwarz Inequality
80	The Fundamental Theorem of Arithmetic
85	Divisibility by 3 Rule
89	The Factor and Remainder Theorems
91	The Triangle Inequality
96	Principle of Inclusion/Exclusion

This set spans combinatorics, geometry, number theory, set theory and logic, analysis, algebra, and mixed foundational material. Some entries are short wrappers around standard-library theorems that already express the right mathematics. Others required more substantial development: finite powersets, finite-set counting, coordinate-plane geometry, finite real inequalities, integer number theory, finite groups, and polynomial reasoning all appear in the current work.

The project has been especially useful because it turns library design into a concrete pressure test. It is easy to say that a theorem prover should have good support for finite sets, elementary number theory, or real inequalities. It is more revealing to ask whether those ingredients are sufficient to prove a named theorem from the Top 100 list in a form that can be checked and replayed. Each completed entry gives us a small but real data point about Acorn's mathematical coverage.

We have also learned that verification and reproducibility should be treated as separate milestones. A proof search may succeed once, but a public formalization needs to survive outside the original search session. In our workflow, Acorn's verify command can search for proofs and write certificates, while check --strict must replay committed certificates without performing new search. This strict replay requirement has shaped how we package results and how we decide when a proof is stable enough to count as complete.

OmegaCombinator's broader research interest is AI for Mathematics, including multi-agent workflows for formalization. The Top 100 project has become a practical testbed for that work. Agents can explore the Acorn library, propose proof strategies, generate helper lemmas, and attempt proof candidates. Human review still matters: we need to decide which lemmas are genuinely reusable, whether theorem statements are well designed, and whether a proof should live in a project file or become part of the standard library. The value of the agent workflow is not that it removes mathematical judgment, but that it expands the amount of proof space we can explore while keeping Acorn as the correctness checker.

For Acorn, this kind of benchmark is useful because it connects language design, library growth, automation, and proof engineering. A successful Top 100 entry is often not just one theorem. It may leave behind an improved API, a more reusable lemma, a better proof pattern, or a sharper understanding of where current automation struggles. This is why we view the project as a contribution to the Acorn ecosystem rather than merely a separate showcase.

The public tracker at 100.aixmath.org records only complete verified entries. Partial results, helper lemmas, and failed attempts are still important for research, but they do not count as finished Top 100 theorems until the public theorem target is proved. That keeps the progress number conservative and meaningful. At the moment, that number is 29/100.

OmegaCombinator plans to continue upstreaming reusable pieces where appropriate, improving proof stability, and using the remaining Top 100 entries to guide future Acorn library work. We are also continuing to develop AI x Math as a public home for seminars, project notes, and research around automated mathematics. You can find the main portal at aixmath.org and our project notes at blog.aixmath.org.

We are grateful to Kevin Lacker and the Acorn project for building a system that makes this kind of fast, public, replayable formalization work possible. If you would like to discuss the project, collaborate with OmegaCombinator, or learn more about our work on AI for Mathematics, contact zecyel@aixmath.org.