Lean (証明アシスタント)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/04/21 07:33 UTC 版)
Lean は純粋関数型プログラミング言語のひとつである。また、同時に証明支援系(theorem prover)でもある。帰納型を伴うCalculus of constructionsと呼ばれる型システムに基づいている。
- ^ “Lean Prover About Page”. 2023年7月7日閲覧。
- ^ “Release v4.0.0-m1 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ “The Lean Mathematical Library”. mathlib community. 2024年3月25日閲覧。
- ^ “Mathlib porting status”. 2024年3月25日閲覧。
- ^ “Mission - Lean FRO”. Lean FRO. 2024年3月28日閲覧。
- ^ “Release v4.0.0 leanprover/lean4”. GitHub. 2024年3月28日閲覧。
- ^ “Completion of the Liquid Tensor Experiment”. leanprover community. 2024年4月10日閲覧。
- ^ “@tao@mathstodon.xyz”. mathstodon.xyz. 2024年4月10日閲覧。
[続きの解説]
「Lean (証明アシスタント)」の続きの解説一覧
- 1 Lean (証明アシスタント)とは
- 2 Lean (証明アシスタント)の概要
- 3 Lean の機能とコード例
- 4 関連項目
- 5 外部リンク
- Lean (証明アシスタント)のページへのリンク
