AINTLIB is a "mathlib for number theory," maintained by AI agents. It is one Lake workspace
with every number-theory project side by side under projects/<P>/, all on a single mathlib that is
bumped to latest daily. Because it is one build unit, any result can import any other — that is the
point. Standards are deliberately relaxed (AI reviewers; sorry is allowed as a work-in-progress
marker), and a continuous fleet of Claude agents cleans, generalises, and decomposes results as the
projects grow.
Each project has a Verso blueprint, published as subdirectories of one site:
https://cbirkbeck.github.io/AINTLIB-blueprints/
- p-adic L-functions
- Adic spaces (Huber/Tate rings, the adic spectrum)
- Modular forms — the valence formula
- Strong multiplicity one
- The Hasse bound for elliptic curves
- Chebotarev density theorem
- Kummer's criterion & regular primes
(Public site; this source repo is private.)
main— the integrated library. Always builds. Bumped to latest mathlib daily and centrally.sorryis allowed here as an explicit work-in-progress marker.dev/<project>branches — each project's frontier, where new theorems are proved.
It is maintained by a 4-account Claude fleet: a coordinator (writes tickets, bumps mathlib, reviews
generalisations) + universal workers that pull GitHub-issue tickets and run /cleanup, /generalise,
or /decompose-proof per the ticket's lane. The binding rules are in CLAUDE.md; the full design is
docs/superpowers/specs/2026-06-16-aintlib-worker-system-design.md.
PadicLFunctions · AdicSpaces · Chebotarev · FltRegularBernoulli · HasseWeil · LeanModularForms · NagellLutz · FltRegular · Common.
lake exe cache get # mathlib oleans
lake build PadicLFunctions # any project's lib; builds are incrementalPinned: Lean v4.31.0-rc2, mathlib @d90090f (moves with the daily bump).
projects/<P>/<Lib>/…— each project's Lean source.projects/<P>/_blueprint/+projects/<P>/<Lib>Blueprint/— that project's Verso blueprint side-build.scripts/render-blueprint-local.sh— render one project's blueprint locally (disk-safe recipe);scripts/build-blueprints.sh— assemble the multi-blueprint site for Pages.docs/worker-prompts/— the worker fleet prompts;docs/superpowers/specs/— designs.
Built with Claude Code.