Lean 4 is an open-source functional programming language and interactive theorem prover that allows developers to write efficient code and prove its correctness within the same environment. Reimplemented entirely in Lean itself, the latest version features a high-performance compiler and a powerful, extensible macro system. While it is widely used by the mathematical community to formalize complex proofs, it has recently emerged as a critical tool in AI research, providing a verifiable “ground truth” for training large language models in automated reasoning and formal logic.