# Tagged Questions

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

18 views

145 views

### An endless loop in a program that search for mathematical theorems and proofs − a milestone? [closed]

I don't know if there exist computer programs working on its own, trying to find and prove theorems, delivering proofs and go on searching for new theorems. But if (when) there are such programs, ...
48 views

### How does one prove that a computational theorem prover is correct?

There are many computational theorem provers, such as Z3 (http://z3.codeplex.com/). Such provers employ many thousands of lines of code. How can one prove that the results are correct and can be ...
94 views

### Status of declarative proof languages in proof assistants

I'm interested in formalising mathematics and logics in a proof assistant, both to get to know a proof assistant and to make an archive of proofs for myself (nothing too fancy, mainly first order ...
37 views

### Random conversions

I came across a question in StackOverflow which states the following, all is based on natural numbers: Given the function rand5 (which produces random natural numbers 0-4), use it to generate a rand7 ...
66 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 ...
196 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 ...
229 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 ...
66 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 ...
287 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 ...
60 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 ...
7k 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 the formal, pedantic language I have to use to ...
269 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 .
327 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 ...
652 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 ...
116 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 ...
230 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 ...