A self-study curriculum spanning the sciences and humanities. Math, physics, chemistry, biology, philosophy, language, and the social world — same concept, three depths:
- Beginner — intuition, visuals, worked examples.
- Intermediate — formal definitions, proofs, exercises.
- Master — graduate-level depth with primary-source citations and Lean formalisation where Mathlib covers.
Live at https://babelbible.org — ~2,559 units across 50 sections (~360 chapters), every produced unit passing a 27-point automated rubric.
Codename: the Lean formalisation library and internal docs still use the codename Codex. Babel Bible is the product name.
babel-bible/
├── README.md ← you are here
├── AGENTS.md ← agent + contributor entry point
├── OVERVIEW.md ← the load-bearing project doc
├── content/ ← curriculum units (~2,559 markdown files, 50 sections)
├── lean/ ← Lean 4 formalisation (library root: `Codex.*`)
├── site/ ← Neutron-based site → babelbible.org
├── docs/ ← specs, briefs, catalogs, plans
├── plans/ ← expansion state, audits, finalization queue
├── manifests/ ← per-unit state, dependency DAG, campaign log
├── lenses/ ← lens/filter system (curriculum views)
├── _meta/, style/ ← notation + editorial voice
├── scripts/ ← validators + content tooling
└── reference/ ← local archive of external sources (gitignored)
- Spec (
docs/specs/UNIT_SPEC.md) declares the unit format and rubric. - Produce — content agents draft units that pass the 27-point automated rubric (
scripts/validate_unit.py). - Integrate — cross-references validated at build time; broken refs fail the build.
- Site — Neutron generates static HTML; deployed to OVH via Teploy.
- Audit — per-section coverage/gap audits under
plans/expansion/.
Each unit packs Beginner / Intermediate / Master content in a single source file. Section markers ([Beginner], [Intermediate+], [Master]) gate visibility. The tier toggle in the site header changes what the reader sees.
The Lean 4 library lives in lean/ (module root: Codex.*). Each Master-tier unit declares a lean_status of full, partial, or none. Mathlib coverage gaps surface in docs/catalogs/MATHLIB_GAPS.md as contribution candidates.
Built with Neutron — single static-site target served by Caddy. Local dev: cd site && npm run dev. Production: npm run build, deploy with teploy deploy (config in site/teploy.yml).
AGENTS.md— entry point: full doc map and reading order (includes a consolidated Current state section).OVERVIEW.md— the canonical project doc; read this when in doubt.docs/specs/UNIT_SPEC.md— the unit format.docs/specs/QUALITY_RUBRIC.md— the 27-point automated checks.plans/expansion/FINALIZATION_PLAN.md— the live production queue.
Dual-licensed:
- Code (
lean/,scripts/,site/) — MIT, see LICENSE. - Curriculum content (
content/) — Creative Commons Attribution-ShareAlike 4.0 (CC-BY-SA-4.0), see LICENSE-content.md.