Tengoku (天国)

Formal mathematics from many Lean projects, translated onto one Lean version and machine-checked.

About

Formal mathematics is mathematics that a computer can check, step by step. It is scattered across many separate projects,
written for different versions of Lean 4. Tengoku (天国) gathers theorems from many formal mathematics projects into one
Lean 4 library on a single pinned toolchain. A theorem is trusted only once the relevant library checks have passed: it
builds with no sorry, uses only the standard axioms, and its assumptions are checked not to contradict.
Every record links to its source at a fixed commit and carries its licence and credit.

Tengoku and Leak are parts of one service: Tengoku is the library, and Leak is
the intended interface. Leak is tooling and a harness for agent-driven proving over MCP, providing search, proof-state
interaction and verification services. It is not the prover; any MCP-capable system can use it.

(Tengoku can be interpreted to mean sky kingdom, or heavenly abode. This represents our ambition for the useful knowledge in this repository to reach the skies.)

Try it

• Add the Leak MCP tools to your agent (free, no sign-up): Leak I searches
  (Loogle + Moogle + ChromaDB), Leak II steps through proofs (Pantograph service with efficient proof state switching),
  Leak IV verifies a script (Lean kernel daemon). All of these services use the Tengoku
  environment, and are provided like this to make it easy for the community to experiment - no SLA or uptime guarantee is provided.

  Connection URLs

  claude mcp add --transport sse tengoku-search https://barkingtree-leak-i.hf.space/sse
  claude mcp add --transport sse tengoku-proof  https://barkingtree-leak-ii.hf.space/sse
  claude mcp add --transport sse tengoku-verify https://barkingtree-leak-iv.hf.space/sse
  

• Search it on the web: competemath.com/tengoku, in plain English or by name.

• Run your own: the service code.

• HTTP API: docs/api.md.

• Download it: clone this repository and run scripts/cache.sh get to download the compiled library.

Contributors

Anyone can contribute, by hand or with AI. Because of the nature of this project, there are many indirect ways
to contribute and support. Interacting with and providing feedback for the main site, as
well as using and improving the Leak services, all support Tengoku indirectly.

We expect that realistic contributions directly to the project via pull requests will require AI assistance. This is because
parts of the repository change before a human can fully understand it. We understand that this creates a barrier to entry for
contributors due to factors beyond their control. We are not really in a position to solve this issue; if you
want to contribute directly, or want to learn about something that interests you, but can't because you don't
have access to AI tools, get in touch - we will try to help if we have the availability.

For every other prospective contributor, you may work on whatever you wish, even if it initially doesn't
seem like it is related to Tengoku (if you have an odd idea or need particular permissions, get in touch with the link above).
However you contribute, it would be useful to make mention of what you are working on, or would like work to be directed
at, in the goals file.

How credit works · Contributing · How a theorem gets in · Code of Conduct · Posting guidelines · Found an issue, or have an idea? · Found a security problem?.

If you are unsure if an issue is a security problem, assume it is.

Learn more

• Why Tengoku does not trust the toolchain: case studies of Lean 4 failures
• How Tengoku stays reliable
• Training on Tengoku: what labs must do, and what we ask
• What Tengoku checks
• The full manual
• Security and licence compliance (OpenChain ISO/IEC 18974 and 5230)
• Acknowledgements: the projects and people Tengoku stands on
• Cite it: 10.5281/zenodo.23050400, or the Cite this repository button

Thanks

Tengoku makes extensive use of the Lean and Mathlib ecosystem - to the authors who make Tengoku possible, thank you.

 Security, with Snyk. Tengoku is proud to be a member of Snyk's Secure Developer Program, which arms open-source maintainers with its advanced developer-security platform.

 Code review and CI repair, with Gitar. Tengoku is proud to have been admitted to Gitar's open-source program, which gives open-source maintainers its AI code-review and CI-fixing agent.

Funding and affiliation

Tengoku is one of the services of CompeteMath. CompeteMath has no intention of generating income with any of its projects. CompeteMath is not affiliated with, nor does it support, any particular organization, corporate entity, or political group. Anyone considering donating or partnering with us should know that Tengoku will not allow any influence over the governance of this repository, nor its accessibility, the integrity of its contents, or Tengoku's goals.

Badges