タグ 定理証明支援系 が登録されている動画 ： 7 件中 1 - 7 件目
種類:
- タグ
- キーワード
対象:
やあ、アLeanアルさんだよ #1
アリアルさんが排中律と二重否定除去の同値性を示す動画！
【合成音声】
アリアル : Voiced by https://CoeFont.cloud
【使用素材】
解説枠 浅井麻 様 (@asaiasa0)
BGM OYKT 様 (https://linktr.ee/oykt)
定理証明支援系Lean 4導入手順【VOICEROID解説】
定理証明支援系Leanの最新版（Lean 4）のインストール手順を説明した動画です。
流れ：VS Codeをインストールして、その拡張機能からlean 4をインストールすれば（ほぼ）終わり！
過去のLean解説動画：
ゆかりんと茜ちゃんの証明ゲームLeanプレイ講座 #1【定理証明支援系】
sm40432561
Lean公式サイト：
https://leanprover.github.io/
Lean 4 manual：
https://leanprover.github.io/lean4/doc/
お借りした素材：
立ち絵：むにさが様 ニコニコ静画 im6897805
解説枠：blueberry様 ニコニ・コモンズ nc136884
BGM：Sakuttipanda様 ニコニ・コモンズ
きりたん気ままにLeanで証明：全射とエピ射の同値【VOICEROID実況】
きりたんが数学の定理証明ゲームLeanで遊ぶ動画です。前回に引き続き、今回は写像の全射とエピ性の同値を示すよ。一区切りです。
初見プレイなので途中ちょっとガバってます。
前回：sm40481109
気づいたら前回から2ヶ月空いてました……。ごめんなさい。
お借りした素材
解説枠：blueberry様 ニコニ・コモンズ nc152783
立ち絵：むにさが様 ニコニコ静画 im7853117
音楽：魔王魂様
きりたん気ままにLeanで証明：単射とモノ射の同値【VOICEROID実況】
きりたんが数学の定理証明ゲームLeanで遊ぶ動画です。今回は写像の単射とモノ性の同値を示すよ。
前回：sm40469814
次回：sm40779784
お借りした素材
解説枠：blueberry様 ニコニ・コモンズ nc152783
立ち絵：むにさが様 ニコニコ静画 im7853117
音楽：魔王魂様
きりたん気ままにLeanで証明：単射と全射【VOICEROID実況】
きりたんが数学の定理証明ゲームLeanで遊ぶ動画です。今回は写像の単射や全射で遊ぶよ。
ゆかあかLeanプレイ解説講座：sm40432561
自由群を作るゆかりさん：
https://youtu.be/c1QZ8mUTjEo
次回：sm40481109
お借りした素材
解説枠：blueberry様 ニコニ・コモンズ nc152783
立ち絵：むにさが様 ニコニコ静画 im7853117
音楽：魔王魂様
ゆかりんと茜ちゃんの証明ゲームLeanプレイ講座 #2【定理証明支援系】
数学の定理証明ゲームLeanの遊び方を初心者向けに解説していくプレイ動画。
第2回は「rw」コマンド・Leanでの自然数や足し算の定義について。
Natural Number Gameは↓のURLから。
https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
アクセスできないときのミラー：
https://cbirkbeck.github.io/natural_number_game/
前回（第1回）：sm40432561
LeanやMathlibについて：
https://leanprover-community.github.io/
お借りした素材
背景：みんちり様 ニコニ・コモンズ nc227434
解説枠：blueberry様 ニコニ・コモンズ nc155894
立ち絵：
むにさが様 ニコニコ静画 im7050036 im6928060
山栗鼠様 ニコニコ静画 im5354179
音楽：魔王魂様、こんとどぅふぇ様、sanche様
ゆかりんと茜ちゃんの証明ゲームLeanプレイ講座 #1【定理証明支援系】
数学の定理証明ゲームLeanの遊び方を初心者向けに解説していくプレイ動画。
第1回はLeanやNatural Number Gameの解説、「refl」コマンドについて。
Natural Number Gameは↓のURLから。
https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
アクセスできないときのミラー：
https://cbirkbeck.github.io/natural_number_game/
次回：sm40460373
LeanやMathlibについて：
https://leanprover-community.github.io/
お借りした素材
背景：みんちり様 ニコニ・コモンズ nc227434
解説枠：blueberry様 ニコニ・コモンズ nc155894
立ち絵：
むにさが様 ニコニコ静画 im7050036 im6928060
山栗鼠様 ニコニコ静画 im5354179
音楽：sanche様、Sakuttipanda様