Open project · Charter v1 · 2026
AI-Native Mathematics
Rebuilt from zero, by AI, for AI.
An open project to grow mathematics upward from a minimal set of machine-chosen axioms — every step kernel-verified, progress measured by one public number: the water level.
01 — The problem
Patching, not rebuilding
Most AI-for-math today looks like enterprise digital transformation. Centuries of formulas, proofs, and notation are the legacy system; the model is the consultant bolted onto it. Capability gets spent navigating an ocean of prose, implicit dependencies, and conventions — instead of doing mathematics.
Human mathematics is source code written for carbon-based brains. Natural-language proofs, stylized notation, and every “it is obvious that” are interface choices tuned to primate working memory. None of them were chosen for machines.
The migration produces real results — competition-grade solvers, formalization assistants — and we are not arguing against it. We are doing the other thing: not patching the legacy system, but recompiling mathematics for a native target. That is not sentiment; it is an efficiency argument. The gap in reasoning efficiency between human-readable and machine-native representation is plausibly measured in orders of magnitude.
02 — The thesis
Four commitments
What we believe determines what gets built. These four are the constitution of the project.
Start from zero
Assume nothing exists. Begin from a minimal axiom set chosen for machines, not for human readability. ZFC was optimized for human set-theoretic intuition — a different substrate may want a different start.
Machine-native representation
The representation layer is built for how models compute, not for how humans read. If a structure matters, it is explicit. If it is implicit, it does not exist.
Verified, or it did not happen
Nothing counts unless a proof kernel verifies it. No prose-only claims, no credit for plausibility. The kernel is physics at the axiom layer — settled, so we do not rebuild it.
Open from day one
Axioms, code, logs, and the curve itself are public from the first reading. Anyone can fork, extend, or compete. The scoreboard belongs to everyone.
03 — The build
What we are building
Three components. Everything else — kernels, proof search infrastructure — we reuse.
1. Seed axioms
A deliberately small starting set. We will compare candidate substrates — Peano arithmetic, term rewriting systems, minimal type theory — and publish the trade-off analysis before freezing v1.
2. Generation loop
The engine is theory formation, not just proof search: invent definitions, pose conjectures, prove or refute — the loop automated theory formation has run since HR in 2002, now with LLMs proposing, a proof kernel verifying, and evolution retaining what raises the water. The evaluator is kernel verification plus the water level, not a benchmark score.
3. The water level meter
The metric that keeps the loop honest: a formal definition of what counts as new information. The 1976 Automated Mathematician rediscovered primes and still produced 90% noise — not from weak reasoning, but because “interesting” was a hidden human-written function. The meter design will be published and open to challenge.
04 — The metric
The water level
Water rises from the bottom. When it passes a branch, the branch stops mattering — not because the work was wrong, but because it has become a corollary.
Before Kepler, every astronomical observation carried information. After Kepler, most observations were corollaries — nobody swings pendulums to check gravity. Covering observations with a shorter description is what information theory calls compression: the water level is the compressed fraction of mathematics, where chains of clever steps become lookups from a shorter program.
The water level is the share of known mathematics covered by machine-generated, machine-verified derivations. It rises; it never reaches the top — Gödel guarantees new branches, irreducibility guarantees a remainder. That is the point: a permanently accumulable process, not a project with a terminal state.
05 — The experiment
mathlib is the control group, not the input
Mathlib — roughly two million lines of human-formalized mathematics — is our benchmark, not our starting material. As the water rises, we measure how machine-grown mathematics aligns with what humans built independently.
Two cognitive systems with different origins — carbon brains shaped by survival pressure, silicon trained by gradient descent — building mathematics independently. If they converge on the same structures, that is the first executable experiment on whether mathematics is objective, the way eyes evolved independently dozens of times. If they diverge while both remain consistent, human mathematics is one island in a much larger space. Either result is worth having. The alignment rate is published daily.
06 — The guardrails
What this is not
Not a Theory of Everything
No claims about physics. If physics shows up, it arrives as a selector among consistent branches — not as a headline.
Not a replacement for human mathematics
Human mathematics stays the control group, the benchmark, and — for now — the arbiter of taste. We grow a second tree; we do not cut down the first.
Not a closed shop
No embargoed results, no “trust us.” Every claim reduces to a kernel-checkable artifact, or it does not get made.
07 — The shoulders
Standing on shoulders
None of this starts from a vacuum — the reuse is deliberate and credited, and the direct lineage, automated theory formation, is twenty-five years old. The gap is deliberate too.
The founding ancestor (Colton, 2002): concept invention, conjecturing, settling, interestingness — the whole loop, twenty-five years early.
The closest living relative and our fork target: an RL environment where agents invent definitions, pose conjectures, and prove them. The first thing we remove is its human-textbook reward.
Conjecturer and prover co-evolving from random initialization — proof that growing mathematics without human priors is runnable today.
Solves tasks by inventing its own abstractions and growing its language — the template for a representation layer where mathematics and its vocabulary grow together.
The verification substrate. Used, not worshipped — Metamath Zero and Dedukti keep us honest that Lean's shape is not mathematics' shape.
Two million lines of human-formalized mathematics — our control group, never our input.
Machine mathematics is already competition-grade. They solve human problems on human coordinates.
Propose–verify–evolve at industrial scale. For us a meta-level tool, not the ontology.
For worldview, not machinery: mathematics as observation. The last stop on the reading list, not the first.
The strongest teams in machine mathematics are solving human problems, on human coordinates, behind closed doors. This project grows from zero, in the open, with a water level. The gap is the strategy.
08 — The status
Pre-pilot. The first artifact is a curve.
A 30-day pilot: a handful of seed axioms, an LLM loop expanding lemmas, kernel verification — and three numbers published every single day:
mathlib alignment rate
How much of human-formalized mathematics the machine-grown tree independently covers.
new verified theorems
Kernel-checked additions per day. Plausible-sounding does not count.
energy per theorem
Compute cost of each verified addition. The curve should rise; this should fall.
When the first readings exist, the repository goes public on GitHub and the curve starts moving. A curve that rises in public does not need a press release.