Leanによる「文芸的プログラミング」の実装
Proof Summit 2025CoqのInductiveでは定義できないinductive型を公理的に定義する方法
Proof Summit 2025解析の定理証明実践@Lean 4
Proof Summit 2025Abduction Prover in Isabelle
Proof Summit 2025Lean4による 汎化誤差評価の形式化
Proof Summit 2025Applicative と等価なtypeclass を作ってAgda で 検証してみました
Proof Summit 2025Coq ユーザが Lean を調べてみた
Proof Summit 2025Specifying Regexes
Proof Summit 2025proof irrelevance.v · GitHub
Proof Summit 2019ProofSummit 2019まとめ
Proof Summit 2019