Theorem prover (proof assistant) is a software which allows to check steps of formal proof. Such programs often contain an interactive proof editor, which makes writing a formal proof easier. Some know theorem provers: Mizar, Coq, Isabelle. For automated theorem provers use the ...
4
votes
3answers
182 views
Is it possible to prove everything in mathematics by theorem provers such as Coq?
Coq has been used to provide formal proofs to the Four Colour theorem, the Feit–Thompson theorem, and I'm sure many more. I was wondering - is there anything that can't be proved in theorem provers ...
0
votes
1answer
61 views
Why do we need tactics, reflection and other techniques when we have Curry-Howard for theorem proving?
First of all, I apologize if this question is slightly misplaced, but this seemed the best place to ask it given the mathematical/theoretical nature of the discussion. Given that the Curry-Howard ...
5
votes
1answer
136 views
Are coinductive proofs necessary?
I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed ...
2
votes
0answers
172 views
Coq transparency issues with type class fields
I am having some issues with, I suspect, transparency of fields in type classes. Consider a type class such as
...
1
vote
0answers
310 views
Consequences of technically proving anything in Coq (exploiting a bug)? [closed]
Technically, it is possible to prove anything in Coq proof assistant http ://coq.inria.fr due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis may ...
16
votes
3answers
598 views
How do proof verifiers work?
I'm currently trying to understand the concepts and theory behind some of the common proof verifiers out there, but am not quite sure on the exact nature and construction of the sort of systems/proof ...
