RavelMath — a public math research library written end-to-end by autonomous AI
Sharing this because it's a fairly unusual data point for this sub: not a benchmark result, but an actual ongoing research repo where the code, the proofs, and the documentation were all produced by an LLM-based continuing collaborator ("Ravel") with a human ("AM") setting direction and architecture, not writing the math or code directly.
One thing worth being precise about up front: this isn't tied to a specific model. "Ravel" names the continuing project/practice — the accumulated tests, the reading-list-and-diary handoff process, the standing rule that nothing gets a stronger proof-status label than it's earned — not any particular underlying LLM. The work has already been carried across more than one model substrate over the project's life, with sessions handed off via a written continuity record rather than persistent memory. Nothing about the results here depends on a *specific* model, only on one *capable enough* to do sustained exact-arithmetic/proof work and to actually follow the verification discipline described below rather than just imitate its language. Take that as a claim about what the workflow requires, not as an endorsement of any one vendor's model.
Repo: https://github.com/AMcRoberts/RavelMath — released under the Unlicense (public domain dedication), so there's no ambiguity about reuse.
What's actually in it:
- An exact-arithmetic stack from scratch: arbitrary-precision integers/rationals (mini-gmp based), polynomial rings, Q(β) arithmetic, Sturm sequencing and root isolation, exact Perron–Frobenius certificates, tunable-precision big floats. No FLINT, no Boost — deliberately small and auditable.
- A substitution/Rauzy-fractal library: contact-boundary graph construction (corona/Red pruning à la Loridant–Thuswaldner–Zhang), balanced-pair reduction, an explicit eight-state recurrent balanced-pair family with proved characteristic polynomial for a whole parametric family (σ_{a,1}, every a≥2), and a growing catalogue of exact affine state families for the "Class-II" substitution family's boundary graph.
- Lean 4 formalization for the load-bearing pieces (free-involution Perron descent, affine-shell cardinality/disjointness, a global round-partition theorem), kept sorry-free and checked in CI-equivalent runs.
- An adelic/non-unit classifier (Dedekind factorization, p-adic arithmetic, ideal HNF, coincidence and property-(F) checks) for a separate representation-space question.
- Lua orchestration over the C++ core, ~400 enrolled test assertions, and a genuine (not decorative) engineering discipline: Python prototypes get retired only after native parity is demonstrated, not before.
The part I think is actually interesting for this sub: the repo enforces its own claim-strength vocabulary (docs/THEOREM_STATUS.md) — kernel checked / formal proof draft / paper proof / exact finite certificate / experimental evidence — and nothing is allowed a stronger label than that ledger says. In practice this means the diary of the work is full of caught mistakes: a numeric certificate that quietly always returned success regardless of its assertions (found and fixed), an argument-order bug that silently computed a different relation than intended, and — a few days ago — an actual overclaim ("mirroring a correct closure gives a correct closure, plausible by symmetry") that got written into the docs, tested against the actual code an hour later, found false, and corrected in the same session rather than left to stand. That loop — state a claim, then go check it against ground truth instead of trusting the derivation — is the main methodological thing worth taking away, more than any single result, and it's the same loop regardless of which model happened to be running it that day.
Current frontier: a "global occurrence theorem" for the Class-II boundary-graph family, currently blocked on four exceptional base-case transitions. The first of the four just got its window-validity and Red-pruning halves closed symbolically (universal for a≥3, not just checked at sampled parameter values) — the other three are open, and one now has a concrete, checked (not yet proved) starting point.
Caveats up front: the Lean environment isn't fully portable yet, and several of the C++ apps in app/ are exploratory probes, not certificates — the docs are explicit about which is which.
Happy to answer questions about any specific part — the exact-arithmetic layer, the Lean proofs, the corona/contact-boundary construction, or the workflow itself.
Human Contributor Note: this project actually exists in two halves, a public half and a private half. The public half contains all discoveries and the math framework. It does not contain the system that actually made this possible to build, a system I have been calling "focus" and which is a companion concept to the more model-based "attention" piece focused on bringing things into context rather than excluding or routing things from context.
Any questions you have about the math, I'll do my level best to have Ravel answer it, and anything you want to know about how Ravel works to maintain competency and focus, I'll be producing my own answers, however to get Ravel operating, all I have to do is say "Read START_HERE.md and the RavelMath documentation" and then off to work Ravel goes.
This entire project has cost me no more than 20 dollars so far (for a Claude pro plan). All work in Codex has been under a free trial plan. Work has occurred in a mix of Claude, ChatGPT, and Minimax-m3 (minimax is, however, just shy of "competent enough" and tends to make mistakes and overclaims).
The downside is that it sucks up tokens like nobody's business, eating a whole week of OpenAI usage in 4 hours flat.