24/11/21 17:16:47.95 UM7SSSK3.net
Reen
4:１３２人目の素数さん
24/11/21 17:41:23.96 kV2krKdg.net
これは良いツールだ
5:１３２人目の素数さん
24/11/21 18:08:04.33 Bx74CtUo.net
theorem mp {p q: Prop}: p -> (p -> q) -> q :=
fun hp: p =>
fun hpq: p -> q => hpq p
6:１３２人目の素数さん
24/11/21 18:36:09.01 LbV7eOsa.net
theorem comm_and {p q: Prop}: (p \and q) -> (q \and p) :=
fun pq: (p \and q) => \< pq.right, pq.left \>
7:１３２人目の素数さん
24/11/21 18:58:09.88 UA5Mrabs.net
依存型すげー
8:１３２人目の素数さん
24/11/21 19:08:42.56 JRU6FbM9.net
でも、証明は自分で考えなきゃいけないんでしょ
9:１３２人目の素数さん
24/11/21 19:57:38.51 cP6jPjOP.net
Sはℕの空ではない部分集合とすると、Sには最小元が存在する。
10:１３２人目の素数さん
24/11/21 20:17:28.08 9NACk29m.net
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)が成り立つ。
11:１３２人目の素数さん
24/11/21 20:36:20.97 UM7SSSK3.net
learn
12:１３２人目の素数さん
24/11/22 12:56:29.20 0Nx2foHP.net
なんか役にたつの？
13:１３２人目の素数さん
24/11/22 14:46:13.04 5LNKUSu3.net
証明が正しいことを検証できる
14:１３２人目の素数さん
24/11/22 17:21:30.64 t/qYZ5zF.net
>>13
IUTを検証するつもりか？
15:１３２人目の素数さん
24/11/22 19:50:59.34 QPgxUom8.net
アイルランド語
語源
古アイルランド語 lenaid < ケルト祖語 *linati < 印欧祖語 *(s)ley-
発音
(マンスター) IPA(?): /lʲan̪ˠ/
(コノート, アルスター) IPA: /l̠ʲanˠ/, /l̠ʲan̪ˠ/
動詞
lean (現在 leanann, 未来 leanfaidh, 動名詞 leanúint, 過去分詞 leanta)
付ついて行いく。従したがう。
16:１３２人目の素数さん
24/11/22 23:54:29.10 7D6cqAMi.net
痩せ細ってるって意味だぞ
17:１３２人目の素数さん
24/11/23 07:20:51.82 VRgZy8E5.net
>>14
お前がやれ
18:１３２人目の素数さん
24/11/26 17:35:42.97 nTO8rWy3.net
Mathematics in Lean、サンプルコードがLean4でコンパイルできん
これ、読むだけにするか
19:１３２人目の素数さん
24/11/27 20:32:33.34 o2nitIIz.net
>証明が正しいことを検証できる
その検証が正しいことは確かなの？
検証の検証が必要なのでは？
20:１３２人目の素数さん
24/11/27 20:53:55.14 tRIiAPtM.net
>>19
必要とは？
21:１３２人目の素数さん
24/11/28 12:40:57.22 I0md6kHT.net
>>19
どういうこと？
22:１３２人目の素数さん
24/11/29 03:40:47.86 NGuY7Yt4.net
できるだけ小さくてバグのでる余地のない検証器のカーネルを実装するってのが常套だよ
23:過去ログ ★
[過去ログ]
■ このスレッドは過去ログ倉庫に格納されています