Skip to main content

Questions tagged [theorem-proving]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1 vote
0 answers
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 ...
AgnostMystic's user avatar
1 vote
0 answers
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 ...
AgnostMystic's user avatar
5 votes
1 answer
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.
Red Banana's user avatar
  • 5,401
0 votes
0 answers
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 ...
ShyPerson's user avatar
  • 495
1 vote
2 answers
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$
Rebel's user avatar
  • 115
1 vote
1 answer
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?
hengxin's user avatar
  • 840
-3 votes
1 answer
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: ...
Alex's user avatar
  • 51
2 votes
1 answer
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$ (...
David G. Stork's user avatar
1 vote
0 answers
134 views

What should be the response of FindEquationalProof?

The code ...
user64494's user avatar
  • 26.7k
0 votes
1 answer
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 ...
David G. Stork's user avatar
0 votes
0 answers
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 ...
atat's user avatar
  • 95
3 votes
0 answers
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 ...
Carlo Beenakker's user avatar
1 vote
2 answers
178 views

Finding a root that makes this huge polynomial negative

I have the following polynomial. ...
Morcus's user avatar
  • 309
6 votes
3 answers
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: ...
mrz's user avatar
  • 11.7k
3 votes
3 answers
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: <...
lotus2019's user avatar
  • 2,141
2 votes
2 answers
101 views

How to deduce cosine theorem with vector?

I want to prove the cosine theorem of triangles with vectors under the following assumptions: ...
lotus2019's user avatar
  • 2,141
19 votes
1 answer
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 (...
Math Gaudium's user avatar
3 votes
0 answers
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 ...
Gravifer's user avatar
  • 872
3 votes
1 answer
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) ...
user64494's user avatar
  • 26.7k
2 votes
1 answer
111 views

How to deduce circle theorems in Wolfram language?

I can deduce the first one by applying FindGeometricConjectures on the following scene: ...
user13892's user avatar
  • 9,443
-2 votes
1 answer
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. ...
Huanca Sullca's user avatar
1 vote
1 answer
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 ...
ilan's user avatar
  • 53
2 votes
0 answers
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: <...
imas145's user avatar
  • 998
7 votes
1 answer
220 views

Using logical equivalence to prove PL statements

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}[,]...
Ethan's user avatar
  • 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 ...
dharmatech's user avatar
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 ...
Ten-Thousand-Hands's user avatar
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: ...
stefan's user avatar
  • 3
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 ...
EGME's user avatar
  • 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 ...
David G. Stork's user avatar
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 ...
J.A.B.'s user avatar
  • 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 ...
Ben Hekster's user avatar
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: ...
Michael L.'s user avatar
9 votes
1 answer
219 views

Proving uniqueness of group identity element

Start, as in the Mathematica 11.3 documentation, with: ...
murray's user avatar
  • 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: ...
Red Banana's user avatar
  • 5,401
10 votes
4 answers
2k views

How can I calculate the limit without using L'Hôpital's rule

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?
Black Marik's user avatar