証明支援系に関することなら何でも
| SUN | MON | TUE | WED | THU | FRI | SAT |
|---|---|---|---|---|---|---|
1  Kitamado | 2 Kitamado | 3  SnO₂WMaN | 4 Kitamado | 5  __pandaman64__ | 6 | 7 |
8 | 9  Palalansoukî | 10 Kitamado | 11 | 12 | 13 | 14  s-taiga |
15 SnO₂WMaN | 16 s-taiga | 17 | 18 | 19  ネスけん。 | 20 | 21  wasabi315 |
22  梅崎直也 | 23  rikitoro | 24 Kitamado | 25 |
- 12/1#lint コマンドの超軽い紹介Lean4 の #lint コマンドについて
- 12/2Lean のマクロと Macro 型についてのかなり短い紹介Lean4 の Macro 型について
- 12/3スマリヤンのシステムについてGitHub - SnO2WMaN/notes-on-smullyanTP: Note on SmullyanTP
- 12/4#html コマンドの概要を雑に説明するLean日報: ProofWidgets の #html コマンドでグラフなどを表示
- 12/5ProofDataで中間的な定義や証明を整理するProofDataで中間的な定義や証明を整理する
- 12/9強制法を用いてカット除去定理を証明するGitHub - iehality/advent2024-algebraic-hauptsatz
- 12/10Leanの短絡評価についてLean 日報: [macro_inline] 属性で短絡評価にする
- 12/14数学的帰納法を末尾再帰にするLean で数学的帰納法を末尾再帰で実装する
- 12/15命題論理と様相論理のラベル付きシークエント計算をLeanで実装/証明する（実装が難航しているため当分延期で…）
- 12/16lean-jaで公開している文献紹介lean-jaのドキュメント紹介
- 12/19Lean4でバブルソートを書く
- 12/21パターンマッチの網羅性検査をAgdaで形式化する（締切に間に合わなそう）
- 12/22何か書きます
- 12/23Lean4 で ICan'tbelieveItCanSort を書くLean4 で ICan'tbelieveItCanSort を書く
- 12/24Aesop タクティクで手軽に自動証明
