Lean 4

Lean 4 is a high-performance programming language and formal proof support system for the efficient formalization and verification of mathematical theorems.

Proof of Formality

This page is auto-translated from [/nishio/Lean 4](https://scrapbox.io/nishio/Lean 4) using DeepL. If you looks something interesting but the auto-translated English is not good enough to understand it, feel free to let me know at @nishio_en. I'm very happy to spread my thought to non-Japanese readers.