Lean 総合スレッド

**１３２人目の素数さん** · 2024/11/21(木) 16:30:48.75

Lean 総合スレッド

**１３２人目の素数さん** · 2024/11/21(木) 17:16:22.87

Leen

**１３２人目の素数さん** · 2024/11/21(木) 17:16:47.95

Reen

**１３２人目の素数さん** · 2024/11/21(木) 17:41:23.96

これは良いツールだ

**１３２人目の素数さん** · 2024/11/21(木) 18:08:04.33

theorem mp {p q: Prop}: p -> (p -> q) -> q :=
　fun hp: p =>
　　fun hpq: p -> q => hpq p

**１３２人目の素数さん** · 2024/11/21(木) 18:36:09.01

theorem comm_and {p q: Prop}: (p \and q) -> (q \and p) :=
　fun pq: (p \and q) => \< pq.right, pq.left \>

**１３２人目の素数さん** · 2024/11/21(木) 18:58:09.88

依存型すげー

**１３２人目の素数さん** · 2024/11/21(木) 19:08:42.56

でも、証明は自分で考えなきゃいけないんでしょ

**１３２人目の素数さん** · 2024/11/21(木) 19:57:38.51

Sはℕの空ではない部分集合とすると、Sには最小元が存在する。

**１３２人目の素数さん** · 2024/11/21(木) 20:17:28.08

Sをℕの部分集合とする。自然数nに対して、命題P_S(n)を以下のように定める:

Sがnを含むならば、Sは最小元を持つ。

すべての自然数nに対してP_S(n)が成り立つことを、数学的帰納法で証明する。
まず、P_S(0)は正しい。なぜならば、Sの要素は自然数であるので、0以上であるからである。
0以上n以下の自然数kについてP_S(k)が成り立つと仮定し、P_S(k+1)を示す。
Sがn+1を含むとする。
Sがn以下の自然数を含むならば、仮定よりSは最小元をもつ。
そうでなければ、n+1がSの最小元である。
よって、P_S(k+1)が成り立つ。

**１３２人目の素数さん** · 2024/11/21(木) 20:36:20.97

learn

**１３２人目の素数さん** · 2024/11/22(金) 12:56:29.20

なんか役にたつの？

**１３２人目の素数さん** · 2024/11/22(金) 14:46:13.04

証明が正しいことを検証できる

**１３２人目の素数さん** · 2024/11/22(金) 17:21:30.64

>>13
IUTを検証するつもりか？

**１３２人目の素数さん** · 2024/11/22(金) 19:50:59.34

アイルランド語
語源
古アイルランド語 lenaid < ケルト祖語 *linati < 印欧祖語 *(s)ley-

発音
(マンスター) IPA(?): /lʲan̪ˠ/
(コノート, アルスター) IPA: /l̠ʲanˠ/, /l̠ʲan̪ˠ/
動詞
lean (現在 leanann, 未来 leanfaidh, 動名詞 leanúint, 過去分詞 leanta)

付ついて行いく。従したがう。

**１３２人目の素数さん** · 2024/11/22(金) 23:54:29.10

痩せ細ってるって意味だぞ

**１３２人目の素数さん** · 2024/11/23(土) 07:20:51.82

>>14
お前がやれ

**１３２人目の素数さん** · 2024/11/26(火) 17:35:42.97

Mathematics in Lean、サンプルコードがLean4でコンパイルできん
これ、読むだけにするか

**１３２人目の素数さん** · 2024/11/27(水) 20:32:33.34

>証明が正しいことを検証できる

その検証が正しいことは確かなの？
検証の検証が必要なのでは？

**１３２人目の素数さん** · 2024/11/27(水) 20:53:55.14

>>19
必要とは？

**１３２人目の素数さん** · 2024/11/28(木) 12:40:57.22

>>19
どういうこと？

**１３２人目の素数さん** · 2024/11/29(金) 03:40:47.86

できるだけ小さくてバグのでる余地のない検証器のカーネルを実装するってのが常套だよ