A Lean 4 + mathlib formalisation of Geb, a categorical programming
language whose first-class notions include "programming language"
itself. The repository develops mathematical content in a style
shaped to be plausibly upstreamable to mathlib4 (via the
Geb/Mathlib/ subtree) or CSLib (via Geb/Cslib/) alongside
downstream-only content (under Geb/Internal/).
See lakefile.toml for the full dependency declaration.
Apache 2.0, matching mathlib4.
docs/index.md— topological narrative of implemented mathematical content.docs/process.md— process rationale and decision history.docs/references.md— Lean library and mathematical reference catalog.
The contributor-binding rules live in three audience-shaped entry-point files at the repo root:
- CONTRIBUTING.md — universal contributor rules (humans + AI agents).
- AGENTS.md — additions for AI coding agents in general.
- CLAUDE.md — Claude Code-specific additions.
Path-scoped rules live in docs/rules/:
lean-coding.md— applies to all.leanfiles.upstream-eligible.md— applies underGeb/Mathlib/,Geb/Cslib/,GebTests/Mathlib/, andGebTests/Cslib/.markdown-writing.md— applies to all.mdfiles.ci-and-workflow.md— applies to.github/workflows/andscripts/.
Claude Code's path-scoped loader at
.claude/rules/ consists of symlinks to the
canonical files in docs/rules/ plus Claude-only delta files
for additions specific to Claude.
See CONTRIBUTING.md. All participants are expected to follow the project's Code of Conduct.
Content in Geb/Mathlib/ is intended for eventual extraction as
mathlib4 PRs. Content addressing computer-science topics
overlapping CSLib targets
CSLib instead and lives in Geb/Cslib/. Code in Geb/Internal/
is not eligible for upstream submission; some of it may eventually be
recast into an upstream-eligible form and moved to Geb/Mathlib/ or
Geb/Cslib/, while other Internal code has no upstream home.