Mathematics Stack Exchange
Mathematics Stack Exchange

Questions tagged [theorem-provers]

Automatic proof checkers verify the validity of formal proofs, while proof assistants aid in the construction of formal proofs. Some popular systems: Mizar, Coq, Isabelle. For automated theorem provers use the (automated-theorem-proving) tag

This tag is for questions concerning automated proof checkers and proof assistants.

An automated proof checker (or proof verifier) is a program designed to check the validity of a formal proof.

A proof assistant is a program designed to aid in the construction of a formal proof, and likely includes an interactive proof editor.

Some popular systems: Mizar, Coq, Isabelle. For automated theorem provers, use the tag.

There is a separate Proof Assistants site.

75 questions
13
votes
4 answers

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 such as Coq? A little extra question is if…
ocharles
  • 231
3
votes
1 answer

Why is automated proof checking so hard?

(Warn: this is not about automated proving which is impossible. It is about the automatized proof checking). For example, there is no automated test developed for Wiles Theorem (aka Fermat last theorem) until now. Why? My naive intuition were that…
peterh
  • 2,683
1
vote
1 answer

lean prover for $\neg (p \wedge \neg p)$

I did this code : section variable p : Prop example : ¬ (p ∧ ¬ p) := assume h : p ∧ ¬ p, show false, from (and.left h) (and.right h) end But I have the following message error : function expected at h.left term has type …
Netchaiev
  • 4,811
0
votes
1 answer

Prove: $\forall x ( R(x,x) \to R(a,a))$

Nãoconsigo entender como se prova este argumento, podem me ajudar: $\forall x ( R(x,x) \to R(a,a))$ Translation: I don't understand how to prove that $$\forall x ( R(x,x) \to R(a,a))$$ Could you help me?
Felix Pinheiro
  • 1