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

0
votes
0answers
18 views

Proof: Majorant- and minorantcriterion for convergence of improper integrals

Let $I$ a interval and let $f,g:I\to \mathbb{R}$ continuous with $0\le g(x) \le f(x) \forall x \in I$. Prove this propostitions: (a) If $\int_{0}^{\infty} f(x)dx$ convergent $\Rightarrow$ $\int_{0}^{\...
-3
votes
1answer
19 views

I solved this by mean value theorem and I'm asking am i right

[![enter image description here][1]][1] [1]: http://i.stack.imgur.com/UihHo.jpg can i solve case 2 by same way like that if b>a for the interval [b,a] ?
-1
votes
1answer
40 views

is it a vector space or not? [closed]

check if this is a vector space or not ? 1- let $v=R=\{(x,y):x,y \in \mathbb{R} \}$ check if $(V,+,.)$ where $(x,y)+(z,w)=(x,y)$ and $k.(x,y)=(k.x,k.y)$ is a vector space or not 2- ...
0
votes
3answers
47 views

Prove that the sum is bounded on $[-1,1]$.

I have the following problem. (a) Prove that the series $\sum \frac{x^n}{(n+1)!}$ is convergent for all $x\in \mathbb R$. We denote $R(x)$ its sum. (b) Prove that $R$ is bounded on $[-1,1]$....
0
votes
0answers
42 views

Prove that $f$ is bounded on $\mathbb R$

I have the following problem. Definition 0.1 Let $f : R\to R $. We say that $\lim_{x_\to +\infty} f(x) = l\in R $ if$$\forall \varepsilon > 0 \ \ \exists A>0: \ \ \forall x \ge A |f(x) - ...
0
votes
2answers
29 views

Accepting that $\lim_{x\to\infty}f(x) = +∞$ prove that $\lim_{n\to\infty}\frac{n^\delta}{\ln^\gamma n} = +\infty$

I have the following problem to prove. Let $\gamma, δ \in \mathbb{R}^\ast_+$ and $f\colon \mathbb{R}^\ast_+\to \mathbb{R}$ defined by $f(x) = \delta x − \gamma\ln x$. Accepting that $\...
1
vote
1answer
61 views

Prove E(x)=pn by taking derivative of Newtons binomial theroem

I have this formula: $E(X)=$$\sum_{k=1}^n k$$n \choose k$$p^k$$(1-p)^{n-k}$ and I am trying to prove $E=(X)=pn$, by taking the derivative of with respect to y: $(x+y)^n=$$\sum_{k=0}^n$$n \choose k$...
0
votes
1answer
29 views

Identity prove by using properties of complex conjugation

So what I need to do is verify this identity here: $(x^2+y^2)(a^2+b^2)=(xa-yb)^2(xb+ya)^2$ for real numbers $x,y,a,b$ I don't know how this can be done through something like $z_1=x+iy,z_2+a+ib$ The ...
0
votes
1answer
11 views

Show that $Fix(ϕ)$ is ether {0}, a subgroup of the form $L = {tv : tR}$ for some $v ∈ R^2$ \ {0} or the full space $R^2$

i have a problem: The fixed point set of $\varphi ∈ Aut(R^2)$ is defined to be $Fix(\varphi) = {v ∈ R^2: \varphi(v) = v}$ Show that $Fix(\varphi)$ is ether {0}, a subgroup of the form $L ...
1
vote
1answer
64 views

prove a polynomial is divisible

How do I prove that if a polynomial $p(x)$ is divisible by $(ax+b)^n$ where $n>1$ then $p'(x)$ is divisible by $(ax+b)^{n-1}$ I have no idea how to prove that but by logic it is obvious that is ...
0
votes
1answer
27 views

Show that the interest rate sequence is defined

I have a problem where I have to show that the interest rate sequence defined by $x_n := (1+\frac{1}{n})^n$ is Cauchy. I think I can apply the binomial theorem to show that but I have no idea how ...
-1
votes
1answer
40 views

Help with Prover9 for weak propositional systems

I am trying to get Prover9 to work, but apparently am not using exactly the correct commands. Can someone give me a hint, please? This is just a test case, but ...
0
votes
1answer
45 views

Prove that Cov$(\sum_{k=j}^\infty \rho^k e_{t-k}, \sum_{k=0}^\infty \rho^k e_{t-j-k} ) = \rho^j \frac{\sigma^2}{1-\rho^2}$, where $e_t$ white noise

Let $e_t$ be a white noise, in other words: E$e_t = 0$, Cov$(e_t, e_{t'})=0$, when $t \not = t'$, Var$(e_t) = \sigma^2$ (do not depends on time t) Let $|\rho| < 1$, $ j>0 $ be constants. ...
0
votes
1answer
45 views

How to prove an expression including Bessel function is positive?

The modified Bessel function of order n of the first kind is given by $$I_n(x)=\sum_{m=0}^{\infty}\frac{(\frac{1}{2}x)^{2m+n}}{m!\Gamma(m+n+1)}$$ where $\Gamma$ is defined by an improper integral, $...
2
votes
1answer
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, ...
4
votes
0answers
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 ...
2
votes
0answers
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 ...
1
vote
1answer
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 ...
2
votes
1answer
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 ...
2
votes
1answer
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 ...
5
votes
1answer
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 ...
0
votes
1answer
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 ...
2
votes
2answers
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 ...
0
votes
2answers
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 ...
1
vote
3answers
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 ...
1
vote
2answers
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 .
6
votes
2answers
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 ...
8
votes
4answers
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 ...
0
votes
1answer
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 ...
8
votes
1answer
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 ...
1
vote
0answers
232 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 ...
22
votes
3answers
1k 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 ...