◎正当な理由による書き込みの削除について:      生島英之とみられる方へ:

Lean 総合スレッド


動画、画像抽出 || この掲示板へ 類似スレ 掲示板一覧 人気スレ 動画人気順

このスレへの固定リンク: http://5chb.net/r/math/1732174248/
ヒント:5chスレのurlに http://xxxx.5chb.net/xxxx のようにbを入れるだけでここでスレ保存、閲覧できます。

1132人目の素数さん
2024/11/21(木) 16:30:48.75ID:f0B7SpBa
Lean 総合スレッド
2132人目の素数さん
2024/11/21(木) 17:16:22.87ID:UM7SSSK3
Leen
3132人目の素数さん
2024/11/21(木) 17:16:47.95ID:UM7SSSK3
Reen
4132人目の素数さん
2024/11/21(木) 17:41:23.96ID:kV2krKdg
これは良いツールだ
5132人目の素数さん
2024/11/21(木) 18:08:04.33ID:Bx74CtUo
theorem mp {p q: Prop}: p -> (p -> q) -> q :=
 fun hp: p =>
  fun hpq: p -> q => hpq p
6132人目の素数さん
2024/11/21(木) 18:36:09.01ID:LbV7eOsa
theorem comm_and {p q: Prop}: (p \and q) -> (q \and p) :=
 fun pq: (p \and q) => \< pq.right, pq.left \>
7132人目の素数さん
2024/11/21(木) 18:58:09.88ID:UA5Mrabs
依存型すげー
8132人目の素数さん
2024/11/21(木) 19:08:42.56ID:JRU6FbM9
でも、証明は自分で考えなきゃいけないんでしょ
9132人目の素数さん
2024/11/21(木) 19:57:38.51ID:cP6jPjOP
Sはℕの空ではない部分集合とすると、Sには最小元が存在する。
10132人目の素数さん
2024/11/21(木) 20:17:28.08ID:9NACk29m
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)が成り立つ。
11132人目の素数さん
2024/11/21(木) 20:36:20.97ID:UM7SSSK3
learn
12132人目の素数さん
2024/11/22(金) 12:56:29.20ID:0Nx2foHP
なんか役にたつの?
13132人目の素数さん
2024/11/22(金) 14:46:13.04ID:5LNKUSu3
証明が正しいことを検証できる
14132人目の素数さん
2024/11/22(金) 17:21:30.64ID:t/qYZ5zF
>>13
IUTを検証するつもりか?
15132人目の素数さん
2024/11/22(金) 19:50:59.34ID:QPgxUom8
アイルランド語
語源
古アイルランド語 lenaid < ケルト祖語 *linati < 印欧祖語 *(s)ley-

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

付ついて行いく。従したがう。
16132人目の素数さん
2024/11/22(金) 23:54:29.10ID:7D6cqAMi
痩せ細ってるって意味だぞ
17132人目の素数さん
2024/11/23(土) 07:20:51.82ID:VRgZy8E5
>>14
お前がやれ
18132人目の素数さん
2024/11/26(火) 17:35:42.97ID:nTO8rWy3
Mathematics in Lean、サンプルコードがLean4でコンパイルできん
これ、読むだけにするか
19132人目の素数さん
2024/11/27(水) 20:32:33.34ID:o2nitIIz
>証明が正しいことを検証できる

その検証が正しいことは確かなの?
検証の検証が必要なのでは?
20132人目の素数さん
2024/11/27(水) 20:53:55.14ID:tRIiAPtM
>>19
必要とは?
21132人目の素数さん
2024/11/28(木) 12:40:57.22ID:I0md6kHT
>>19
どういうこと?
22132人目の素数さん
2024/11/29(金) 03:40:47.86ID:NGuY7Yt4
できるだけ小さくてバグのでる余地のない検証器のカーネルを実装するってのが常套だよ

lud20250304194247
このスレへの固定リンク: http://5chb.net/r/math/1732174248/
ヒント:5chスレのurlに http://xxxx.5chb.net/xxxx のようにbを入れるだけでここでスレ保存、閲覧できます。

TOPへ TOPへ  

このエントリをはてなブックマークに追加現在登録者数177 ブックマークへ


全掲示板一覧 この掲示板へ 人気スレ | Youtube 動画 >50 >100 >200 >300 >500 >1000枚 新着画像

 ↓「Lean 総合スレッド 」を見た人も見ています:
【DEATH】デスメタル総合スレッドpart7【総合】
【三菱自動車】総合スレッド108【Drive@earth】
【GHC】プロレスリング・ノア総合スレッド【GREAT VOYAGE】
【総合】GOD EATER:ゴッドイーター愚痴・不満スレ33喰目
【総合】GOD EATER:ゴッドイーター愚痴・不満スレ28喰目
川上稔と作品総合スレッド The 443th Horizon
Aqours クラブ活動 LIVE & FAN MEETING ~ Landing action Yeah!! ~ イベント総合スレ83日目
Aqours クラブ活動 LIVE & FAN MEETING ~ Landing action Yeah!! ~ イベント総合スレ93日目
長岡亮介総合スレッド
松屋総合スレッド267
新日総合スレッド2626
位相空間論☆総合スレッド
Temu総合スレッド ★3
新日総合スレッド3012
線形計画法 総合スレッド
Realme総合スレ Part.11
若手女優総合スレッド Part4
類体論総合スレッド part3
◆社会人野球総合スレッド 135◆
YouTuber将棋棋士 総合スレッド
jubeat総合スレ 376th Tune
東京の銭湯総合スレッド Part54
数学検定(数検)総合スレッド Part.14
麻布高校開闢以来の秀才 伊理正夫 総合スレッド
ARIA 総合スレッド Navigation.246
REFLEC BEAT 総合スレ 271th BATTLE
競技プログラミング総合スレッド@数学板
Android ゲーム総合スレッド part71
Go To Eatキャンペーン 総合スレ★61
Go To Eatキャンペーン 総合スレ★87
REFLEC BEAT 総合スレ 262nd BATTLE
【ゼニディール】YOUDEAL総合スレ
Go To Eatキャンペーン 総合スレ★39
プリンセスメーカー 総合スレッド Part.22
Yale大学 天才 成田悠輔 の数学力 総合スレッド
【数学検定】数学検定(数検)総合スレッド Part.12
【数学検定】数学検定(数検)総合スレッド Part.8
【東京大学教授】 斎藤毅 総合スレッド 【数論幾何】
【Roland】ローランド総合スレッド 19 【老国】
神奈中/神奈中東/神奈中西 総合スレッドPart33
【なでしこJAPAN】日本女子代表総合スレッド 405
サンスイ ■ SANSUI総合スレッド 69 ■ 山水
【総合】GOD EATER:ゴッドイーター1798喰目
ウェイトリフティング総合スレッド Part.2
【追い込み】LEC総合スレッドunit74【開始】
【なでしこJAPAN】日本女子代表総合スレッド 411
【なでしこJAPAN】日本女子代表総合スレッド 412
【1134kHz】文化放送 総合スレッド Part.2【JOQR】
【Leaf GEOMETRY】はきかエロゲ総合スレ11 ©bbspink.com
【総合】GOD EATER:ゴッドイーター1781喰目
【FF16】 FINAL FANTASY XVI 総合スレッド PART1
Jazzピアニストにして数学者 中島さち子 総合スレッド
【ゲーム】Storyシリーズ総合スレ 5【TeamLava】
【入口】マイクプリ・HA・AD/DA総合スレ Part.4
[2V] BMW 2バルブRシリーズ総合スレ-18[AirHead]
女性数学者総合スレッド 佐々田、伊藤、石井、中島、山下、宮岡、小谷
【本スレ】風来のシレン6総合 134F【Switch/steam】
【UEVR / UUVR】VR mod 総合スレ Part3【PC / SteamVR】
Metal Gear Solid メタルギアソリッドシリーズ総合 part389
【次スレくらい】ROCKET LEAGUE ロケットリーグ総合スレ part60【立てろ高卒】
ラブライブ!スクールアイドルフェスティバル PERFECT Dream Project 総合スレ Part.1.6
代数学総合スレッド Part6 (566)
数学ダジャレ総合スレ

人気検索: star sessions loli julia Child 無撫 スク水 熟年 teen 露出 海 聖心女子大生 隲剰ィェ驥? 縺励♀繧?
20:22:42 up 86 days, 21:21, 0 users, load average: 10.47, 11.24, 11.67

in 0.07883095741272 sec @0.07883095741272@0b7 on 071309