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
0
votes
2
answers
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 ...
-3
votes
0
answers
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)$.
- 7
2
votes
0
answers
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 ...
-1
votes
0
answers
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.
- 11
0
votes
0
answers
35
views
Is my verification of an argument OK? And, a question about a Computer System to verify arguments
I found the following exercise in the Discrete Mathematics and Functional Programming book by Thomas VanDrunen.
3.14.4
(a) $\forall x \in A, P(x) \land \lnot Q(x)$
(b) $\forall x \in A, x \in B$
(c) $\...
- 53
0
votes
0
answers
20
views
A questions about using basic rules to simplify complicated boolean algebra:
When I was in the digital logic class at school, the teacher taught me basic Boolean algebra rules and some common simplification methods and then assigned some homework, but when I went to prove it ...
1
vote
0
answers
45
views
How can we guessing when function is differentiable?
I am trying to guess when a function is differentiable: I need this in order to prove that using the implicit and logarithmic differentiation method we can prove that
$$
\dfrac{\operatorname{d\!}}{\...
0
votes
1
answer
70
views
Prove $\sup(A^2) = (\sup(A))^2$ [closed]
So we let A be non empty set of R that’s bounded. Define $A^2=\{a^2\mid a \in A\}.$ How do we prove that the $\sup(A^2) = (\sup(A))^2.$ I've been approaching this by showing that $(\sup A)^2$ is an ...
- 1
1
vote
0
answers
36
views
Lean: Prove that if homomorphisms are equal as functions, then they are equal as homomorphisms.
Let's say I have a simple magma structure defined as follows:
structure Magma :=
(carrier : Type u)
(op : carrier → carrier → carrier)
together with a magma ...
- 316
0
votes
2
answers
52
views
How to calculate the variance of this probability model?
There is such a rule in the game "Genshin Impact"：
Every three materials a can be fused into one material b.
Suppose the amount of original material are a, which is the corresponding $\...
- 83
1
vote
1
answer
117
views
understanding $\Pi$- and $\Sigma$-types via arithmetic interpretation
I'm trying to understand $\Sigma$- and $\Pi$- types in dependent type theory. On the bottom of page 9 of this document, there are two equations giving a justification for the names of $\Pi$- and $\...
- 313
0
votes
2
answers
36
views
Why is the composition also a function
I was working on the following task:
Let $f: N \rightarrow P$ and $g: M \rightarrow N $ be functions.
Definition of a function:
In mathematics, a function from a set X to a set Y assigns to each ...
- 49
0
votes
0
answers
27
views
How to prove the statement "If 𝐵 = 𝑃𝐴𝑃<sup>−1</sup>, and 𝑃 is nonsingular, then det(𝐵) = det(𝐴)" if it is true or false? [duplicate]
Statement: If 𝐵 = 𝑃𝐴𝑃−1, and 𝑃 is nonsingular, then det(𝐵) = det(𝐴)
Similar Example: Suppose A and B are similar matrices. Then there exists an invertible matrix P such that B = PAP-1
solution:
...
- 115
1
vote
1
answer
118
views
Do logical connectives in type theory not form well-formed formulas like they do in classical logic?
I have been doing exercises in Lean theorem prover where I was introduced to type theory.
There is a variety of type theories, this question applies to those that behave similarly to Lean's dependent ...
- 33
3
votes
2
answers
232
views
The formula for $g\frac{d}{dg}g\frac{d}{dg}...g\frac{d}{dg}f(g)$
Yesterday, I asked if there is a formula given by a finite sum for the expression. Having experimented with Wolfram Alpha I found that it can be represented as
$$ \sum_{j=0}^{n}a_{j}g^{j}\frac{d^{j}}{...
- 1,009
3
votes
1
answer
212
views
How we can we prove that for any $b > a, x > 0$, $\frac{2}{\pi} (1-\frac{a}{b})<\sup|\frac{\sin(ax)}{ax} - \frac{\sin(bx)}{bx}|<4(1-\frac{a}{b})$
I want to prove this for any $x > 0$ and $b > a > 0$:
$$
\frac{2}{\pi} (1-\frac{a}{b})<\sup|\frac{\sin(ax)}{ax} - \frac{\sin(bx)}{bx}|<4(1-\frac{a}{b})
$$
I tried the derivation to find ...
-1
votes
2
answers
136
views
Is $\mathbb{Z} ⊂ \mathbb{Q}$ true in formal proofs? How do formalized systems capture this relationship?
Informally, mathematicians treat Integers like a subset of rational numbers.
But according to the standard, formal construction of $\mathbb{Q}$, $\mathbb{Q}$ is an equivalence class over $\mathbb{Z} \...
- 151
1
vote
1
answer
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 ...
- 4,771
-3
votes
2
answers
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:
...
- 11
-1
votes
1
answer
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 ...
0
votes
0
answers
32
views
question about flooring a certain kind of numbers [duplicate]
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:
$$\...
- 176
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 ...
- 11
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 ...
- 143
-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.
- 357
-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!
- 29
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.
- 147
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 ...
- 137
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)
- 43
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 ...
- 4,868
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.
- 524
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 ...
- 5,675
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 ...
user732763
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 ...
- 772
-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 ...
- 85
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 ...
- 11
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 ...
- 161
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}\...
- 85
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 ...
- 12.6k
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 ...
- 117
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:
:= $(\...
- 75
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 ...
- 157
0
votes
0
answers
486
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....
- 41
0
votes
2
answers
505
views
How to prove that the XOR problem for dimension d is not lineary seperable
The 2 dimensions xor problem can be converted to 4 equations which is possible to prove that are not possible to solve
...
