✍
🙃
Lean で数学的帰納法を末尾再帰で実装する
🥐
Lean Prover で Cantor の対関数に逆写像があることを示す
🥯
lake update 時に toolchain does not have the binary というエラーが出たときの対処例
🤙
Lean 4 でカントールの定理
🩺
Lean4 で print デバッグをする
🏄
mdbook に Lean4 のコードブロックを Playground で実行するボタンを追加する
🎇
静的サイトジェネレータ(SSG)で作成したサイトにおいて， Lean4 のシンタックスハイライトを効かせる方法
☄️
Lean Prover コマンド紹介
🔃
選択ソートと，それがソートアルゴリズムであることの証明を Lean Prover で実装する
🔢
if 式で定義された関数の性質を Lean Prover でどう証明するか
🐦
フィボナッチ数列の2通りの定義が等しいことを，Lean4 を使って証明する
📑
Mathematics in type thoery 日本語訳
📑