Lean 4は、高性能なプログラミング言語兼形式的証明支援システムで、数学定理の形式化や検証を効率的に行うためのツールです。