# 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

6 questions
31 views

### How to Prove The Complement Of The Domain Is Complement Of The Image If f Is Bijective

It seems true that $f(\overline{X}) = \overline{f(X)}$ for $f:A\rightarrow B$ and $X$ is any subset of $A$ if and only if $f$ is bijective.But I couldn't write it as a formal way like epsilon argument....
72 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 ...
132 views

### Can I use Coq to formalise the proofs from Terence Tao's Real Analysis textbook?

I'm working through Terence Tao's Real Analysis textbooks which start from Peano's axioms and build up from there and I was wondering can I use Coq to formalise and verify my proofs but without having ...
44 views

### Isabelle/HOL sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont

I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/...
### Prove that $q_A = {q_l}^2$ in geometric series of areas and corresponding side lengths of equilateral figures
Let $l_n$ be a geometric series of the side lengths of any equilateral two-dimensional figure and $A_n$ be a geometric series of the area of the said figure. Prove that $q_A = {q_l}^2$, whereas \$q_A ...