LL Future (2008-08-30)今井宜洋 (yoshihiro503) 次　: sm4505381 (shelarcy) 最初: sm4481852 (LL Future 開会宣言) マイリスト: mylist/8224180http://ll.jus.or.j...

schemeできるっていうてるやん よく考えて命名規則作らないとすぐ詰まりそうな言語だなぁ w T...

アリアルさんが排中律と二重否定除去の同値性を示す動画！【合成音声】アリアル : Voiced by https://CoeFont.cloud【使用素材】解説枠　浅井麻 様 (@asaiasa0)BGM　OY...

たすかる アリアルさん(ｶﾜｲｲ∨ｶﾜｲｸﾅｲ)↔︎(ｶﾜｲｸﾅｸﾅｲ→ｶﾜｲｲ)ﾔｯﾀｰ! やっぱりタクティクでやるのか〜 難しかったやつだ 証明ゲーム…人狼みたいなんやろなあ(棒) あっこれ専用IDEじゃなくてVSCodeなのか、モダンだあ おつ...

定理証明支援系Leanの最新版（Lean 4）のインストール手順を説明した動画です。流れ：VS Codeをインストールして、その拡張機能からlean 4をインストールすれば（ほぼ）...

飛んできた rfl 今見てきたけどleanとC++みたいだね 良いぞー Lean良いよね haskellみたいだった ゆかlean ちゃんとプライベートリポジトリにバックアップするやで・・・（n敗 なんなら紙に書いてたからな（パンチカードは編集しづら...

きりたんが数学の定理証明ゲームLeanで遊ぶ動画です。今回は写像の単射や全射で遊ぶよ。ゆかあかLeanプレイ解説講座：sm40432561自由群を作るゆかりさん：https://youtu...

ムスカ大佐の気持ち VSCodeのフォントファミリーと拡張機能のおかげで文字の違和感が消えている・・・ 証明モードを使わない書き方、カリーハワード同型対応みが感じられて好きだけど読みづらいから好きじゃない 解説2回まで見たけどさっぱり きりもいいたん...

数学の定理証明ゲームLeanの遊び方を初心者向けに解説していくプレイ動画。第2回は「rw」コマンド・Leanでの自然数や足し算の定義について。Natural Number Gameは↓のUR...

Lean上では定義というより、得体の知れない2変数関数にいくつか公理が与えられてる感じなのかな？ はえー 続き待ってる うぽつ aと0は書かなくてもいいんやな いい動画だった なんとなくノリが分かってきた ここすごいな この動画見てずっと遊んでる ...

数学の定理証明ゲームLeanの遊び方を初心者向けに解説していくプレイ動画。第1回はLeanやNatural Number Gameの解説、「refl」コマンドについて。Natural Number Gameは...

WhiteSpaceと同時に書けそう 日本語で数学やるやつおらんから無問題 ←そんなやつはじめから学会にはおらんｗ 強すぎｗｗｗ     refl     , うp主経験者？ つよ 乗法の定義にもよるが、帰納法か？ すごいな ・・・これ薬学...

定理証明器Coqを使った、証明のデモです。　[Coqのダウンロードhttp://coq.inria.fr/]　　[Coqのブログ「にわとり小屋のプログラミング日記」http://d.hatena.ne.jp/yos...

trivialではないのか 今のCoqだと "No more subgoals" なので少しさみしい 講義でやった〜 Propを使うときはVariableよりHypothesisを使ったほうがわかりやすい ここはapplyよりassumptionを使...