Tengoku

Tengoku (天国) is one self-contained Lean 4 library. It was seeded from Mathlib and every package Mathlib pulls in, and it grows by verified translations of theorems from every open formalization project we can find, and by direct contributions. Its purpose is continuously improving, reliable context for automated theorem provers: one library to search, one toolchain, one definition of “trusted”.

This page is the full breakdown. The repository README is the quick start.

Using it

• Search on the web: competemath.com/tengoku searches the whole library by meaning or by type shape, with the trust status on every result.
• Leak I, the free MCP service: the same search from inside your editor or agent, at https://barkingtree-leak-i.hf.space/sse. No auth configuration required. The index is managed by CompeteMath and follows every merge of the tree.
• API: GET https://competemath.com/api/tengoku/search?q=… returns JSON, no key. Input and output shapes: docs/api.md.
• Self-serve services: proof states (Leak II) and verification (Leak IV), hosted or on your own machine: github.com/mikael-bashir/leak-services. What each Leak harness does is on the Leak page.

The tree

• No Dependencies: Everything lives in the Tengoku/ folder. The only external requirement is the pinned Lean toolchain (v4.34.0-rc2).
• Self-Contained Seed: Mathlib and its dependencies were copied in once. SEED.md tracks their origins, but we no longer sync with them. Original declaration names are unchanged.
• Strict Trust: A theorem is “trusted” only if it compiles cleanly in this tree with no errors, no missing proofs (sorry), and no extra axioms.
• New Additions: Saved in Tengoku/<Library>/. Every module is built.
• Zero-Build Caching: You never build from scratch. Nightly releases cache the compiled tree. Run scripts/cache.sh get to download the latest cache and only build your changes, or use scripts/pin.sh to sync perfectly and build nothing.
• Live Updates: Every merge publishes its compiled difference instantly. This keeps the hosted Leak services synced with main in minutes without compiling.

Tiers

Every record already has a real proof from somewhere. The tier says whether Leak has stamped it:

• tentative — a real proof from a real source (every record carries a source_url pointing at it) that Leak has not re-verified on the pinned toolchain yet.
• staging — a translation of a real proof, produced by Emissary-Archangel: the original lived on another toolchain; this is the same claim restated and re-proved on Tengoku’s, and it passed two gates — it compiles cleanly, and an independent entailment check confirms it proves at least as much as the original. Not yet in any module.
• trusted — compiled and certified by the pinned toolchain’s own kernel, in this tree. Mathlib lives here by definition.

Promotion only goes one way, tentative or staging → trusted, and only by Leak actually building the record’s module. Nothing is trusted by assumption.

Record shape

Each line of every data/**/*.jsonl file is one record:

{
  "name": "...",
  "statement": "theorem ... : ...",
  "proof": ":= by ...",
  "status": "tentative | staging | trusted",
  "library": "...",
  "source_url": "...",
  "toolchain": "..."
}

Contributing

Every change is a pull request, and the repository does the checking:

• The gate (about three minutes): every added record has the right shape, a source on the allowlist, a name its statement declares, no duplicate of a trusted name; no sorry,axiom, native_decide, macros, notation or anything that runs code; a signed-off commit; no authorship line ever removed.
• The merge queue: compiles exactly the mathematics a PR adds, on the pinned toolchain, before it lands. A PR the queue ejects is left open with the reason.
• The blind re-proof test (original theorems only): name up to ten headline theorems; a fresh agent that sees only the statement, with the library’s own search, proof-state and verification services, gets about five minutes each. If it re-proves every one, the library already reaches all of it and the PR is rejected; if at least one resists, it passes. The whole attempt is recorded and the gate re-derives the verdict from the raw transcript. Translations of existing libraries are exempt — a translation is never new mathematics.
• Authorship stays with you. A docstring above each theorem names the human author, the AI system used if any, and a link to your identity (GitHub, LinkedIn, ORCID, or your CompeteMath ID). It travels with the record into the tree, permanently.
• Translating a whole library is automated: register the source, and Emissary-Archangel translates it theorem by theorem, each verified translation arriving as its own pull request.

Details, commands and the record files to edit: CONTRIBUTING.md, how Tengoku is tested, the blind re-proof test, top-ups.

Why v4.34.0-rc2

Nearly every serious formalization project depends on Mathlib and tracks a Mathlib-compatible toolchain, so the reachable union of theorems is largest on the Mathlib release most projects have already moved to, not on a novel toolchain. When the tree was created, Mathlib’s master and its dependencies were pinned to v4.34.0-rc2, and the largest live projects (FLT, Carleson, PFR) matched it exactly. Everything on another toolchain is reached by translation.

Sources

100+ source libraries, 500,000+ theorems. A declaration whose proof contains sorry anywhere is dropped at harvest, never mislabelled as tentative.

Tools

• tools/harvest.py clones a Lean repository and extracts every theorem and lemma — name, statement and full proof — by a syntactic scan, no build needed; rerunnable against any library at any time.
• tools/harvest_prove2me.py pulls proved theorems and their accepted solutions from Prove2Me’s API; tools/split_jsonl.py shards any file too big for GitHub.
• scripts/seed.py, scripts/generate.py, scripts/promote.py: the re-runnable seed, the module generator, and promotion (build the record’s module, then move it to trusted).

Independence

Tengoku and the wider CompeteMath ecosystem were founded by one person. There is no intention of making money from this project, and it is not affiliated with, nor does it support, any organization, company or political group. No donation or partnership buys influence over the repository’s governance, accessibility, or the integrity of its contents.

competemath/tengoku