A proof assistant is software used for creating and checking formal proofs; examples include Coq and HOL. This tag is not to be used for requesting assistance on finding proofs.
Stats
created |
1 year ago |
viewed |
7 times |
editors |
0 |
Top Answerers
more »Recent Hot Answers
Why is it so difficult to write complete (computer verifiable) proofs?Is there a known way to formalise notion that certain theorems are essential ones?
How do they verify a verifier of formalized proofs?
How do they verify a verifier of formalized proofs?
Function extensionality: does it make a difference? why would one keep it out of the axioms?
more »
Related Tags
lo.logic × 10
soft-question × 3
proof-theory × 3
coq × 3
type-theory × 2
formalisation × 2
more related tags