Tengoku

Tengoku (天国 — “heaven”) is an open-source Lean 4 formal knowledge tree, with a few key features:

1. 1)Unifies many open-source Lean 4 libraries, translating them to the newest Lean 4 toolchain that Tengoku tracks.
2. 2)Welcomes contributions from anyone (get in touch if you have any questions).
3. 3)Continues to expand autonomously with Leak integration.