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

learn more… | top users | synonyms

1
vote
3answers
29 views

Greatest value of the binomial coefficient.

How should I prove the greatest value of the binomial coefficient $C(n,r)$ occurs for $r=\left[\cfrac{(n+1)}{2}\right]$ ?
0
votes
2answers
26 views

Prove Maximum term in the expansion.

How should I prove the maximum term in the expansion of $(x+a)^n$ where $ax>0$ is the term $C(n,r)x^{(n-r)}a^r$ for which $r= \left[\cfrac{(n+1)}{(n/a)+1} \right]$ ?
1
vote
1answer
48 views

Prove an ideal is maximal

Question Prove the ideal $\mathrm I=\{f \in \mathrm R| f(2)=0 \}$ of $\mathrm R=\{f(x) | f: \Bbb R \to \Bbb R $ is continue} is maximal. DO NOT use the $1$st isomorphism theorem. ...
0
votes
1answer
29 views

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 ...
0
votes
0answers
18 views

I need to prove by induction $(n-1)!\int_0^1{dx_1\:\ldots\:\int_0^1{dx_n\:\delta(x_1+\ldots+x_n-1)}}=1$ [duplicate]

Prove by induction $$(n-1)!\int_0^1{dx_1\:\ldots\:\int_0^1{dx_n\:\delta(x_1+\ldots+x_n-1)}}=1$$ I can check the cases $n=1,2,3$ but I don't know how the prove the general case. Thank you very much! ...
2
votes
1answer
63 views

Proving the propositional tableau sound and complete

There is something fundamental that stops me from understanding the proofs for the propositional tableau. (1) soundness proves that all theorems that can be proved are valid (2) completeness proves ...
0
votes
0answers
29 views

How to handle “positive difference or zero”?

Particularly in the type $\mathtt{nat}$ within the proof assistant Coq, I encounter an operation on nonnegative integers that we can define as $d(m, n) = \max(0, m - n)$. I think that without ...
5
votes
1answer
163 views

Proving that e.g. 421 is prime in a formal system

I'm working in the formal system Metamath, and in the course of learning about number theory I've become acquainted with theorems, such as Bertrand's postulate, that require hand-calculation that a ...
0
votes
1answer
48 views

Help me prove this principle with other Hilbert system principles

I have two choices: 1.to show that this principle is correct with other Hilbert system principles the first order $\forall x(A \to B(x)) \to (A \to \forall x B(x))$ (original screenshot) OR 2. to ...
1
vote
2answers
122 views

Automatic theorem prover for proving simple theorems?

Is there a simple software that I could use to practice proving theorems in my course of mathematical logic? Basically what I need is ability to 1) define what axioms and laws I am allowed to use in ...
0
votes
2answers
44 views

Why this first-order logic formula is not correct?

I'm studing computer science at university, in specific Artificial Intelligence. We are using Otter as Theorem prover. I'm having some problems formalizing this: "John, Mary and Derek are three ...
1
vote
3answers
634 views

Prove « If P(A) is a subset of P(B) => A is a subset of B » [duplicate]

I need to prove «If P(A) is a subset of P(B) => A is a subset of B», generally, I understand the main way I should prove it, but the problem is in formal, pedantic language I have to use to prove ...
1
vote
2answers
140 views

“Points E and F lie on the sides BC and CD rectangle ABCD, the AEF is an equilateral triangle”

Points E and F lie on the sides BC and CD of rectangle ABCD, the AEF is an equilateral triangle. M is the midpoint of the AF. Prove that the triangle BCM is equilateral .
0
votes
0answers
35 views

Theorem provers and summations

The following is a relatively simple example of a result that we can easily see is true, but for which I do not know if an ATP can make sense of (namely, if it can even be expressed within the usual ...
5
votes
2answers
160 views

natural language proof assistant

I was wondering whether there has been any attempt to create a proof assistant that you write in it, in english, I mean you write your proof the usual way in TeX(maybe use a 'simpler english') then ...
6
votes
3answers
314 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
90 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 ...
7
votes
1answer
190 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
197 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 ...
18
votes
3answers
721 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 ...