theorem-proving
-
入职问题
-
Coq：证明如果 (A, B) = (C, D) 那么 A = C /\ B = D
-
在 Agda 中证明当且仅当的错误情况
-
Coq 定理证明：peano 算术中的简单分数定律
-
Lean 中简单的基于 refl 的证明问题（但不是 Agda）
-
如何使用先前的引理正确简化 coq 目标？
-
精益中有根据的递归
-
ATS 证明：如果需要大于或等于，为什么这个是静态的？
-
在 Agda 中，我如何证明 cons after uncons over coinductive list(a.k.a Stream) 是身份？
-
如何在精益中证明 r → (∃ x : α, r)
-
你如何理解 coq 量词 `forall P: Set -> Prop`？
-
基本伊莎贝尔序列极限证明
-
这种空集的形式化在 Agda 中是否正确？
-
如何在Haskell中使用反驳来引导类型检查器？
-
在 Coq 中，是否有与 Rabs、Rineq 合作的策略？
-
Idris：有没有办法在等式证明中引用抽象变量？
-
在 Coq 中将 `not A` 转换为 `A -> False`
-
idris 中列表的简单等式证明（证明 xs ++ [x] = ys ++ [y] -> x = y -> xs = ys）
-
为什么这个证明不需要外延性？ （阿格达）
-
为什么在 Agda 中模式匹配有时 "essential"？