Gnosis math sandbox vs Mathlib vs Std
This is a boundary statement, not a ranking: each layer optimizes for different goals.
| Mathlib | Std / batteries | Gnosis MathSandbox |
|
|---|---|---|---|
| Goal | Broad mathematics library for the Lean community | Lean standard library extensions | Small Init-first graph with explicit Mathlib-debt tracking |
| Imports | Mathlib is the center of gravity | Std/Batteries adjacent to Init |
No Mathlib in the hub closure |
| Fit | General mathematics | Shared prelude utilities | Product-integrated, migration-oriented reduced layer |
When to use Mathlib: you need existing theorems across analysis, algebra, topology, etc.
When to use the Gnosis math sandbox: you want a fast, checkable subgraph, CI that rejects accidental Mathlib imports, and a documented path to peel dependencies into GnosisMathPrelude or local lemmas.
Std/Batteries sit between Init and Mathlib; the Gnosis sandbox currently stays on Init for the hub (see MATH_SANDBOX.md) — expanding to Std is a deliberate policy change.
Lake packages (heritage vs minimal)
open-source/gnosis/lean |
open-source/gnosis/lean-minimal |
|
|---|---|---|
| Mathlib | require mathlib |
None (fast CI / local checks) |
| Role | Full ForkRaceFoldTheorems corpus |
Init-only sandbox roots (MathSandbox, SocioTechnicalSandbox, MathSandboxExtras, …) |
| Validate | Optional lake build MathSandbox |
pnpm run validate:lean-minimal (README) |
Sources live under lean/Lean/; the minimal package symlinks that directory into its Lake layout.