Tengoku (天国)

An AI-first formal mathematics library for Lean 4 agentic theorem provers.

About

Formal mathematics is mathematics that a computer can check, step by step. It is scattered across hundreds of separate projects, written for different versions of the language, Lean 4. Tengoku brings them together in one verified library on one version, so that agentic theorem provers can use all of it at once. A theorem in Tengoku is declared trusted (or Leak-trusted) if it compiles from scratch in the self-contained Tengoku tree, on one of the pinned Lean toolchains listed in the badges above, with no sorry, only the standard 3 axioms, and passing checks intended to catch contradictory assumptions.

One of the things we would like to see is that Tengoku significantly improves the proving capacity of an ATP, compared to when it uses Mathlib. We also hope that the unification of many disparate libraries makes it easier for ATPs to bridge seemingly unrelated mathematics, and the discovery of new mathematics. Finally, we hope Tengoku acts as a continuously improving, reliable context for automated theorem provers. By reliable, we mean a system designed to be exceptionally cynical of all dependencies, even the Lean 4 kernel and elaboration ecosystem - why and how we do that.

(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

Leak is the intended interface to Tengoku.

Add the 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 guarantees
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.