# Questions tagged [theorem-proving]

The tag has no usage guidance.

35 questions
Filter by
Sorted by
Tagged with
1 vote
81 views

### Leveraging Mathematica's Capabilities for Building an Advanced Mathematical Database and Theorem Proving Syst [closed]

This is going to be an important and interesting question about the theorem proving capabilities of Mathematica and may be it has been asked before here but with the advent of LLM's the question ...
• 229
1 vote
80 views

### Scope of Mathematica for verifying a textbook level attempted proof

I'm not an expert in Mathematica but use it often for routine things .Of late I got immenesley interested in the capabilities of Mathematica for verifying proofs, especially those that are ...
• 229
125 views

### Can we find validity proofs by means of rules of inference with FindEquationalProof?

Can we find proofs such as: Using FindEquationalProof? My guess is "yes" but I don't know what would be the "axioms" here nor how would we write this in Mathematica.
• 5,401
42 views

### Symbolic solutions to systems of Boolean constraints?

Is it possible to solve a system of Boolean constraints symbolically? I'm trying to solve systems like the following, where $X$ is the unknown Boolean expression I'm trying to find, $a, b, c$ are the ...
• 495
1 vote
113 views

### Solving a-two-variable equation in primes

How solve the following equation in Mathematica (preferably in one line) for pairs of $(x,y)$ such that $x$ and $y$ are primes? $x^3-y^4=1$
• 115
1 vote
116 views

### Is there any Mathematica API for Z3?

Z3 has bindings for various programming languages, e.g., C, C++, Java, Python, and so on. Are there any for Mathematica? Or how to implement one?
• 840
297 views

### Proving conjecture on number series

I have a conjecture that Stephen Lucas's identities for Pi and its convergent could be generalized as follows: ...
• 51
122 views

### Derive Parseval's theorem in one dimension

Parseval's theorem (in one dimension) is a fundamental result in the theory of Fourier transforms. If $f(t) \Leftrightarrow F(\omega )$ are Fourier transform pairs and $t$ (time) and $\omega$ (...
• 41.6k
1 vote
134 views

The code ...
• 26.7k
86 views

### Using the mathematical typography of formal logic

As asked in this question, I strongly prefer to use "mathematical" typography in Mathematica over text-based ("computer science") typography. Nevertheless, it sometimes fails for ...
• 41.6k
77 views

### Can Mathematica’s automated theorem prover and assistant work with the axioms of real (or complex) numbers?

axioms of real numbers The question pretty much says it all. If I can make Mathematica do simple limit proofs that would be a good start. Of course what I’d really like to do is turn this loose on the ...
• 95
75 views

### Can I use FindInstance to prove an algebraic identity?

This question arose from a [now removed] MathOverflow discussion, where a Null result from a FindInstance query was used to prove that $f(x_1,x_2,\ldots x_n)\neq 0$ has no solution in $\mathbb{R}$. My ...
1 vote
178 views

### Finding a root that makes this huge polynomial negative

I have the following polynomial. ...
• 309
1k views

### The integer ababab (a,b>0) is always divisible by 7, without remainder

The integer $ababab$ $(a>0,b>0)$ is always divisible by $7$, without rest. I tried to prove this by: ...
• 11.7k
335 views

### Verify triple product rule

I'm trying to verify triple product rule $$\left(\frac{\partial x}{\partial y}\right) \left(\frac{\partial y}{\partial z}\right) \left(\frac{\partial z}{\partial x}\right) = -1$$ with the equation: <...
• 2,141
101 views

### How to deduce cosine theorem with vector?

I want to prove the cosine theorem of triangles with vectors under the following assumptions: ...
• 2,141
461 views

### Programming language prototyping in Mathematica

Are you aware of any projects using the Wolfram language resp. Mathematica as an environment to explore the design of programming languages - in particular languages with a focus on mathematics (...
• 487
415 views

### Can Mathematica be used as a proof assistant?

Mathematica have an extensive gallery of mathematical results, as well as a strong rule-based deduction system. Since v12.*, automated proving features have been added to it too. I believe for ...
• 872
178 views

### Axiomatizing naturals

Trying to implement the naturals in Mathematica, I follow E. Mendelson, Introduction to Mathematical Logic, Ch. 3, Par. 1. Here is my code for the axioms (exept the induction axiom) ...
• 26.7k
111 views

### How to deduce circle theorems in Wolfram language?

I can deduce the first one by applying FindGeometricConjectures on the following scene: ...
• 9,443
142 views

### Proving an integral identity [closed]

Assuming $f$ is continus on $[0,\pi]$, show that $$\int_{0}^{\pi }xf(\sin x)dx=\frac{\pi }{2}\int_{0}^{\pi }f(\sin x)dx$$ I tried to demonstrate it using integration by parts, but I did not succeed. ...
1 vote
135 views

### Counting real roots of bivariate polynomial

For a proof, I'm working with a polynomial $p(x,m)$ and I need to show that: For any $m\in (0,6)$, $p_m(x)\equiv p(x,m)$ has a unique real root in $(0,1/2)$. I find that this is true by using Reduce ...
• 53
245 views

### Natural deduction with FindEquationalProof

Out of curiosity, I'm trying to implement a natural deduction prover in Mathematica using FindEquationalProof. So far, I've implemented a few of the easier rules: <...
• 998
220 views

I'm trying to use those Logical equivalence as axioms to prove some PL statements, In this case I followed the examples in the documentation that didn't use the build-in logic functions$\{\text{And}[,]... • 225 7 votes 3 answers 1k views ### Basic theorem proving in Mathematica? Let's say we have the following: p is prime n > 1 (n is an integer) p = nq (I.e. p is a multiple of n) It can be proved that ... • 919 6 votes 1 answer 163 views ### FindEquationalProof to prove divisor theorem I'm trying to implement proofs of concepts for Equational Proofs on some basic number theory theorems. One such example is: "let a and b be positive integers and let d = gcd (a, b). If t divides ... 0 votes 1 answer 408 views ### Implicit Function Theorem I think I am stuck here right now: The exercise is to use implicit differentiation to determine y' considering the following equation: I managed to do this with: ... 4 votes 0 answers 94 views ### Four color theorem in Mathematica [closed] The four color theorem is a theorem about graphs (as in graphs and networks) and it was proved with the aid of a computer. To date, there is no hand-checkable proof. The software that was used to ... • 647 2 votes 0 answers 150 views ### FindEquationalProof with implications Motivated by this question in mathematics, my Mathematica question is essentially this one, but alas the answer to that isn't quite adequate. I'm not interested in verifying that a proof is valid or ... • 41.6k 7 votes 1 answer 442 views ### FindEquationalProof with Logic in Wolfram Mathematica I try to "make" proof in Wolfram Mathematica. Thats a proof: if a->b and b->c then a->c I tried ... • 71 6 votes 3 answers 430 views ### Why Can't Mathematica Resolve this Simple Quantified Expression? I've been using Mathematica as a hobbyist, off and on, for some time. So while I'm by no means an expert I've used it long enough to know that what might seem obvious to me is not necessarily obvious ... 5 votes 1 answer 256 views ### Implementing the field axioms with FindEquationalProof? I am fiddling around with FindEquationalProof, currently trying to prove some basic statements for fields. I have a set of axioms which almost constitutes the field theory axioms: ... • 867 9 votes 1 answer 219 views ### Proving uniqueness of group identity element Start, as in the Mathematica 11.3 documentation, with: ... • 11.9k 11 votes 2 answers 276 views ### Clues on theorem proving tools? I'm trying to prove$[a \cup (b \cap c ) = (a\cup b)\cap (a\cup c)]\$ with Mathematica. But I don't know what function I should use. I've rewritten the sentence in the following way: ...
• 5,401
I need to prove this limit without using L'Hôpital's rule: $$\lim_{x\to 0} \frac{(1+a\,x)^{1/4} - (1+b\,x)^{1/4}}{x} = \frac{a-b}{4}$$ How can I do it in Mathematica?