# 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

75 questions
Filter by
Sorted by
Tagged with
74 views

### Let $a, b, c$ are positive real numbers, such that $a+b+c=1$. Then prove that $\frac{a-bc}{a+bc} +\frac {b-ca}{b+ca} +\frac {c-ab}{c+ab} \leq \frac32$ [closed]

Let $a, b, c$ are positive real numbers, such that $a+b+c=1$. Then prove that $\frac{a-bc}{a+bc} + \frac{b-ca}{b+ca} + \frac{c-ab}{c+ab} \leq \frac32$ Who can help me ? I dont know what inequality ...
64 views

### Prove $f(a+b)=f(a)f(b)$ if $f′(x)=f(x)$ and $f(0)=1$ [closed]

Consider $f:ℝ \rightarrow ℝ$ is a positive and differentiable function with condition $f′(x)=f(x) \ \forall x \in ℝ$, and condition $f(0)=1$. Prove for every $a,b \in ℝ$ that $f(a+b)=f(a)f(b)$.
46 views

### Using the Principle of Well Order, show that for all $n \in N$ it holds that $4^n -1$ is divisible by 3.

Using the Principle of Well Order, show that for all $n \in N$ it holds that $4^n -1$ is divisible by 3. I have already defined the set of counterexamples $C$, then I proved that for $n=1$ the ...
67 views

### Proving a limit by using three function theorem

$$\lim_{x\to\infty}\left(\sin\left(x+\frac{1}{x}\right)-\sin(x)\right)=0.$$ I would like to prove this equation but got stuck on making right inequality for this question.
35 views

1 vote
191 views

### 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 ...
227 views

### Prove $(p → (q → r)) ↔ ((p ∧ q) → r)$ with lean4 [closed]

I try to solve the examples from chapter for from the online guide while learning lean4. But I can't solve this one. I'm as far as: ...
66 views

### Proving diagonalization and inreversibility in matrices [closed]

I'm trying to prove two statements related to matrices but I can't find a good way to prove it: $$T:R^{2}\rightarrow R^{2}$$$$S:R^{2}\rightarrow R^{2}$$ Are linear transformations. What is the ...
32 views

Our math teacher was teaching us about the floor function and after finishing all the important parts we started to do some exercises by ourselves and there was this problem which we all did wrong: $$\... 0 votes 0 answers 32 views ### meaning of “modulo” in Formal Methods. related to this question What is meaning of modulo specifically in the context of Tamarin prover: "Proofs are constructed using backward search with support for reasoning modulo equational ... 6 votes 1 answer 152 views ### Why are let binders part of the kernel in Coq/Lean? I've been looking into the implementations of CIC-based theorem provers - mainly Coq and Lean - and it seems that both of them have let binders as part of the kernel, with their own typing and ... -1 votes 1 answer 147 views ### How to prove \tanh^{-1}(\sin x)=\sin^{-1}(\tan x) [closed] Here's what I attempted:$$ y =\tanh^{-1}(\sin x)\tanh y=\sin x$$But I don't know what to do after this. Please help me. -2 votes 2 answers 52 views ### Prove that |x|\le a [closed] How can I prove this? |x|\le a, \space \space \:-a\le x\le a\:,  \space \space a\in\mathbb{R}. Thanks! 1 vote 1 answer 44 views ### Are there two norms in any space that neither of them is subordinate to the other? Can you prove if no or give an example if yes? Obviously, this should be an example of an infinite-dimensional space, since in a finite-dimensional space, any two norms are equivalent. 1 vote 1 answer 458 views ### Proving first order logic in coq I want to prove something like: Theorem new_theorem : \forall (A B: \text{Prop}), ((A \wedge B) \iff (B \wedge A)). in coq. I know, i could just type firstorder., but could i prove this in coq ... 0 votes 2 answers 111 views ### proving that \sum_{k=0}^{n}{{n \choose k}{n+k \choose k}}=\sum_{k=0}^{n}{2^k{n \choose k}^2} [closed] proving that$$\sum_{k=0}^{n}{{n \choose k}{n+k \choose k}}=\sum_{k=0}^{n}{2^k{n \choose k}^2}$$(prove can be combi or algebraic) 1 vote 1 answer 331 views ### Translating "John is an adult man" into First Order Logic and Prover9 input [closed] I am working on translating a really simple English statement into First Order Logic, which is- "John is an adult man" My first order logic axioms are the following- ... -1 votes 2 answers 60 views ### How to prove a formula for the midpoint of a line between two vectors how to prove that OP1 + 0,5 * P1P2 = OC? C is the midpoint of P1P2. Thank you Click here for the image that illustrates the problem 0 votes 1 answer 396 views ### DISPROVING "Every odd positive integer is the sum of a prime number and twice the square of an integer" Providing a counter-example is enough to disprove a statement. However, it is not the only we of disproving. For example, if the statement is "\sqrt{2} is a rational number", then we can disprove it ... 1 vote 0 answers 58 views ### "modulo" meaning in context of Formal Methods. I am a beginner in the field of Formal Methods in Computer Science. In the literature, I often encounter phrases, such as "... modulo equation theory". Example are: SMT solver -- "Satisfiability ... 1 vote 0 answers 44 views ### Asking help with Riemann Integration [duplicate] i need help with this theoretical exercise with Riemann integration, hope you can help me. Thanks. Prove that if f:\mathbb{R}\rightarrow\mathbb{R} is continuous \vert f\vert Riemann integrable ... 2 votes 2 answers 681 views ### Prove cycling in a Rubik's cube How can I prove that if you apply some algorithm over and over again on a solved Rubik's cube, the cube will be solved? I mean mathematically not conceptually. 1 vote 0 answers 85 views ### The take lemma needs a coinductive proof In Are coinductive proofs necessary?, the answerer claimed that we cannot prove inductively the take lemma: Two streams that agree on all initial subsequences of given length are the same. I was ... 0 votes 1 answer 50 views ### Prove: T_1 = T_2 If (X,T_1), (X,T_2) are compact and Hausdorff for T_1 and T_2 which are comparable prove T_1 = T_2. Well my idea was to create a function F between (X,T_1) and (X,T_2) that carry one ... 1 vote 0 answers 142 views ### How to prove r \implies (\exists x : \alpha, r) in Lean I'm trying to prove the logical statement r \implies (\exists x: \alpha, r), where r is a Prop (a proposition or statement) and \alpha is a ... -4 votes 3 answers 906 views ### prove that if m and n are integers and m+n is odd then m-n is odd. [closed] prove that if m and n are integers and m+n is odd then m-n is odd. -2 votes 1 answer 97 views ### Prove xy\leq \frac{x^p}{p} + \frac{y^q}{q} Let p,q>1,\ \frac1p+\frac1q=1, and x,y>0. Prove that xy\leq \frac{x^p}{p} + \frac{y^q}{q} by using natural log, definition of concave function, and the fact that natural log is a concave ... 0 votes 2 answers 53 views ### How to prove this formula. Formula is for evaluate limits which answers are e to the power something. I would like to ask you about how to prove this formula. I come up with this formula when i was browsing internet. It works when i used it on given examples, but i would like to know if it works in ... 0 votes 2 answers 38 views ### formal definition prove for \lim_{a \to \infty} \{a_n\} = a also applies to \{-a_n\} \to -a By definition of any sequence \{a_n\}: if \lim_{n \to \infty} a_n = a, then for all values \epsilon > 0, there exists a value N \in \mathbb{N} such that for all values n > N then |a_n ... 2 votes 4 answers 80 views ### Proving the equation using binomial theorem I want to prove this theorem using Binomial theorem and I've got trouble in understanding 3rd step if anyone knows why please explain :) Prove that sum: \sum_{r=0}^{k}\... 6 votes 1 answer 454 views ### Why typeclasses rather than inductive types to define mathematical structures in Lean? I am not sure whether this is the right forum for this question, but I am not sure where else to ask (There is no Lean forum afaik). In the Lean Prover mathlib library, typical mathematical ... 0 votes 1 answer 30 views ### 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 ... 0 votes 0 answers 173 views ### Cosets form a group if normal subgroup [duplicate] Given a group G and its subgroup H that creates cosets, prove that cosets form a group iff H - is a normal subgroup. I've tried to find any good prove but I failed - most of the sources (including ... 3 votes 3 answers 58 views ### Prove of a theorem of a geometrical place I am having issues to prove the back of this theorem: Let ABC be a triangle and fixed D∈AB. The Geometric Place of the X-points that form with D and an arbitrary point S∈AC an ... 1 vote 1 answer 217 views ### predecessor and multiplication prove I have trouble, when attempting to : 1- prove mult defines the multiplication function. 2- Prove pred defines the predecessor function. 1- for mult: Base Case: mult 0x= 0 Inductive case: := (\... 0 votes 1 answer 47 views ### Is it sufficient to prove P(x) \geq a if we already know P(x) > a? Is it sufficient to prove P(x) \ge (\text{or} \le) a if we already know P(x) > (\text{or} <)a? For example, to prove$$ \forall n \ge 1 , \sum_{i=1}^{n}\frac{1}{i^2} \le 2  Suppose I ...
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....