# 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

79 questions
Filter by
Sorted by
Tagged with
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 ...
34 views

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

One of my friend told me to check and prove whether $$$\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.$$$ ...
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 ...
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....
• 43
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 ...
• 140
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 ...
• 354
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 ...
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 ...
38 views

• 151
1 vote
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 ...
• 4,819
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 ...
32 views

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 ...
• 127
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 ...