Lean（最新版はLean 4）は強力な型システムを備えた汎用プログラミング言語です。そればかりではなくて、証明支援系としての機能も同一の型システムをベースにして実現しています。AgdaやCoqもまた、型システムに基づく証明支援系／プログラミング言語です。…