About this library

Alphabeta Math holds 20,760 definitions, theorems, proofs, examples and counterexamples across 1246 pages. Every proof is written as numbered steps, each ending in a bracketed note naming what that step follows from. Dependencies are declared in machine-readable form, so the corpus is one acyclic graph you can walk in either direction. It grows in batches and a great deal of mathematics is still missing.

AI usage and limitation

The mathematics here is written by AI and checked by AI. Statements and proofs are drafted by large language models working from published sources, then read by other models, then audited by a human before publication.

The mechanisms described below exist to make errors rare. They cannot make them impossible. Language models are probabilistic, and a proof that survives every check can still be wrong. Read this library the way you would read a careful but unfamiliar author: the argument is on the page, so check it.

Every item carries two provenance labels, one for the statement and one for the proof, so a theorem taken from a textbook is distinguishable from a claim a model formulated. Generated statements are never load-bearing: nothing else in the library is allowed to depend on one.

Declared dependencies also make errors survivable. When something turns out to be wrong, everything resting on it can be listed exactly, so a correction stays bounded. Every item carries a Report an issue control, and reports reach us directly.

Self-containment

Almost every result is proved from material already established in the library rather than from a citation you would have to chase. Where a proof leans on something, that something is usually a page or two away, in the same format, with a proof of its own.

The exceptions are labelled. 129 published items are recorded but not proved here, stated with a citation because other results need them, and marked in fuchsia with a ‡ along with everything downstream of them. 257 items cite material developed later in the reading order and are marked in sky with a ↗, again with their consequences. You never have to guess which dependencies were established here.

Every item and page also carries a dependency level, shown in the page tables, in each group’s dependency graph, and in the list of what an item depends on. If a proof uses something you have not met, the result it rests on sits lower down, so you can drop a level, read that, and come back. Researchers can go straight to a result and see its exact prerequisites; students can enter at their own level and climb.

Proof generation and verification

Pages are built a level at a time by a pipeline written in TypeScript. The code owns coverage, gates and retries; models are dispatched to scaffold, write, audit, judge and adjudicate, and never to decide whether a stage has passed. A stage that fails its gate does not advance.

Scaffolding and source gathering

A model plans a page against reputable published sources, records the exact sections it read, and enumerates the results those sections contain.

Scaffold and source auditing

A second model reads the plan and the harvest, checks the sources resolve, and names anything thin or missing. Gaps are repaired before writing starts.

Authoring

Statements and proofs are written against that plan. A mechanical checker parses every proof, resolves each declared dependency, and rejects any step that leans on a later one.

Auditing

Models that did not write the page read it, with a reviewer above them adjudicating findings and repairing wrong mathematics.

Dual judge lanes

Two judges from different model families read each result alongside the material it cites, working to break the proof rather than approve it. They run independently and never see each other's verdicts.

Adjudication

Every rejection is answered on the record as a real fatal defect, a minor one, or a false positive. A fatal defect is repaired and re-judged before the item can be published.

Scope sweep

The last stage re-reads already-published pages for claims the new material has made false, such as a page saying the library does not yet define something it now defines.

A human audit gates publication and is the one step every published item has in common. The whole per-level process is animated in how a level is built, and a single proof is followed from draft to repair in authoring a proof.

Licence and cost

Everything here is free to read, with no account and no paywall. The content is licensed CC BY-NC-SA 4.0, which allows reuse and adaptation for education, study, teaching and personal work; commercial use needs approval first, and the licence page sets out both. The project is self-funded; the donation page explains how to help with the running costs. Nothing here is or will be gated behind it.