Skip to main content

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

Filter by
Sorted by
Tagged with
0 votes
0 answers
8 views

Open source implementations of euclidean geometery automated theorem provers.

I plan to work on extending a theorem prover which is specialised in generating proofs for questions based in euclidean geometry which is taught to high school students to introduce them to the ideas ...
Janam Zaveri's user avatar
-1 votes
0 answers
34 views

Trying to check whether equation holds or not. [closed]

One of my friend told me to check and prove whether $\begin{equation} \sum_{k_1+k_2+k_3=n;\\ k_1, k_2 \neq n}(\begin{array}{c}n\\{k_1, k_2,k_3}\end{array})x^{k_2-k_1}(-2\delta)^{k_3}=2.\end{equation}$ ...
vibhu srivastva's user avatar
2 votes
1 answer
46 views

How to prove that the feasible set of a two-asset portfolio is a hyperbola?

The question comes from ‘Mathematics for Finance: An Introduction to Financial Engineering’ by Marek Capiński (Author), Tomasz Zastawniak. The book does not give a complete proof, and I did not find a ...
bokabokaboka's user avatar
2 votes
1 answer
61 views

Unclear step in the proof of Inverse Function Theorem

There is one step the necessity of which I don’t understand in the proof of Inverse Function Theorem in Jerry Shurman’s $Calculus$ $and$ $Analysis$ $in$ $Euclidean$ $Space$ (available here https://www....
WhyNót's user avatar
  • 43
2 votes
1 answer
189 views

What is machine-assisted formalization of proofs good for? And when to do it?

I have been watching Terry Tao's lecture on machine-assisted proofs https://www.youtube.com/watch?v=AayZuuDDKP0&t=1460s. However in terms of the formalization of proofs via systems like Lean or ...
yomath's user avatar
  • 140
0 votes
0 answers
45 views

First order logic formalization problem

I have to formalize the following problem for the SPASS theorem prover (first order logic): "On an island there are exactly two type of people: knights, who always say the truth, and knaves, who ...
selenio34's user avatar
  • 354
0 votes
2 answers
104 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 ...
Batyrbek Allamzharov's user avatar
2 votes
0 answers
51 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 ...
Marcos Daniel Castaeda Ramirez's user avatar
0 votes
0 answers
38 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) $\...
calebjosue's user avatar
0 votes
0 answers
21 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 ...
Lesen Liu's user avatar
1 vote
0 answers
49 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\!}}{\...
Alex Quchuloria's user avatar
0 votes
1 answer
93 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 ...
Liza Zee's user avatar
1 vote
0 answers
39 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 ...
Jan Matula's user avatar
0 votes
2 answers
58 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 $\...
Barry Alen's user avatar
1 vote
1 answer
175 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 $\...
Nate Glenn's user avatar
0 votes
2 answers
37 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 ...
alex1888's user avatar
0 votes
0 answers
28 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: ...
Ralph Henry's user avatar
1 vote
1 answer
126 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 ...
primu47's user avatar
  • 43
3 votes
2 answers
238 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}}{...
Artur Wiadrowski's user avatar
3 votes
1 answer
226 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 ...
Mohamed Farouk HASNAOUI's user avatar
-1 votes
2 answers
145 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} \...
user1636815's user avatar
1 vote
1 answer
231 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 ...
Netchaiev's user avatar
  • 4,819
-1 votes
1 answer
67 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 ...
WoodySilva's user avatar
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: $$\...
infinite's user avatar
  • 176
0 votes
0 answers
33 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 ...
sarnuel10's user avatar
6 votes
1 answer
170 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 ...
nonagon's user avatar
  • 143
-1 votes
1 answer
165 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.
langhtorn's user avatar
  • 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!
Fiera28's user avatar
  • 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.
dasfex's user avatar
  • 147
1 vote
1 answer
526 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 ...
David's user avatar
  • 137
0 votes
2 answers
116 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)
Furnitcher's user avatar
1 vote
1 answer
341 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- ...
Sushant Dahiya's user avatar
-1 votes
2 answers
65 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
maxmustermann134's user avatar
0 votes
1 answer
410 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 ...
Hussain-Alqatari's user avatar
1 vote
0 answers
61 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 ...
Mohit Kumar Jangid's user avatar
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 ...
Giuliano Vittori's user avatar
2 votes
2 answers
803 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.
pgp1's user avatar
  • 524
1 vote
0 answers
96 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 ...
user1868607's user avatar
  • 5,965
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 ...
user avatar
1 vote
0 answers
155 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 ...
Enrico Borba's user avatar
-4 votes
3 answers
978 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.
guest world's user avatar
-2 votes
1 answer
98 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 ...
ImBananaBtw's user avatar
0 votes
2 answers
57 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 ...
Emo Gma's user avatar
  • 11
0 votes
2 answers
39 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 ...
NewDev90's user avatar
  • 161
2 votes
4 answers
84 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}\...
Michael W's user avatar
6 votes
1 answer
522 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 ...
user56834's user avatar
  • 13.5k
0 votes
1 answer
31 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 ...
Felix Pinheiro's user avatar
0 votes
0 answers
174 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 ...
JohnIdlewood's user avatar
3 votes
3 answers
59 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 ...
Isabela Marton's user avatar
1 vote
1 answer
226 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: := $(\...
Jared's user avatar
  • 75