Skip to main content
24 votes
Accepted

Programming language prototyping in Mathematica

General Some general answers and comments first. 1 Are you aware of any projects using the Wolfram language resp. Mathematica as an environment to explore the design of programming languages - in ...
Anton Antonov's user avatar
11 votes
Accepted

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

One may regard this question as the test of the system ability of proving theorems, but there is another view to understand what lies beneath this theorem. Then we figure out that the problem is quite ...
Artes's user avatar
  • 57.3k
9 votes

FindEquationalProof with Logic in Wolfram Mathematica

You don't need FindEquationalProof to this end, it is enough to use the quantifiers. ...
user64494's user avatar
  • 26.4k
8 votes
Accepted

Basic theorem proving in Mathematica?

Mathematica does have such a thing, though it's unfortunately not as trivial as one would hope, as that: FindEquationalProof cannot prove theorems involving arithmetic operators by default As ...
DrMrstheMonarch's user avatar
7 votes

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

...
Akku14's user avatar
  • 17.3k
7 votes

Proving uniqueness of group identity element

Let us consider the axioms for a group: groupTheory={ForAll[{a,b,c},g[a,g[b,c]]==g[g[a,b],c]], ForAll[a,g[a,e]==a], ForAll[a,g[a,inv[a]]==e]}; As shown in ...
Fred Simons's user avatar
  • 10.2k
6 votes

Clues on theorem proving tools?

You can compose TautologyQ and Equivalent ClearAll[bEq] bEq = TautologyQ @* Equivalent; ...
kglr's user avatar
  • 396k
6 votes
Accepted

Verify triple product rule

The following is a automation of the proof here. No need to make use of $p V=R T$. eq = Dt@{z == z[x, y], y == y[x, z], x == x[y, z]} \begin{array}{l} dz=dx \frac{...
xzczd's user avatar
  • 66.2k
6 votes

Solving a-two-variable equation in primes

FindInstance cannot prove that there are no solutions, especially when the domain of solutions is the set of primes. More acceptable approach would be: ...
Artes's user avatar
  • 57.3k
5 votes

FindEquationalProof to prove divisor theorem

This is more a draft answer to your question than a full answer. Two observations: first, while I'm hardly any expert on evaluation in Mathematica, Mathematica seems to try to evaluate the terms given ...
ShyPerson's user avatar
  • 495
4 votes

Clues on theorem proving tools?

FindEquationalProof is available as an option: ...
ShyPerson's user avatar
  • 495
4 votes

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

Simplify[Mod[FromDigits[{a, b, a, b, a, b}], 7]==0, {a, b} ∈ PositiveIntegers] True BTW,...
cvgmt's user avatar
  • 73.1k
4 votes
Accepted

Solving a-two-variable equation in primes

Indeed, this can be done in one line: FindInstance[x^3 - y^4 == 1, {x, y}, Primes] {} No solution in the primes.
user64494's user avatar
  • 26.4k
4 votes
Accepted

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

Here you go. The definition of Boolean Logic comes directly from the documentation of FindEquationalProof: ...
ShyPerson's user avatar
  • 495
3 votes

Verify triple product rule

Simplify[D[p[v, t], v]*D[v[p, t], t]*D[t[p, v], p],Assumptions -> p*v == r*t] (*-1*)
Ulrich Neumann's user avatar
3 votes

Finding a root that makes this huge polynomial negative

Obviously you can not calculate differences with such high exponents using machine precision. Therefore you must rationalize your coefficients . However, your coefficients have only a limited ...
Daniel Huber's user avatar
  • 51.9k
3 votes

Finding a root that makes this huge polynomial negative

Redefining your function ...
IntroductionToProbability's user avatar
3 votes

Derive Parseval's theorem in one dimension

The following is my trial for automating the manual deduction here. You can press Ctrl+Shift+t to transform the output to TraditionalForm to make it look good. <...
xzczd's user avatar
  • 66.2k
3 votes
Accepted

Axiomatizing naturals

Here's a first draft of an answer. Induction will be used as the proof technique. Since Mathematica uses an equational prover, there's no direct way to use induction. What will be ventured here are ...
ShyPerson's user avatar
  • 495
3 votes

How to deduce circle theorems in Wolfram language?

It seems that MMA can not find the general result but a special situation such as PlanarAngle equal to 30 Degree. Here is my test. ...
cvgmt's user avatar
  • 73.1k
3 votes

Why Can't Mathematica Resolve this Simple Quantified Expression?

There is a workaround. ClearAll[x, y]; ForAll[{x, y}, x > 0 && y > 0, x*Log[y] == y*Log[x]];Resolve[%, Reals] False
user64494's user avatar
  • 26.4k
3 votes

Implementing the field axioms with FindEquationalProof?

As I understand it, the field axioms cannot be axiomatized this way. But others are trying other ideas.
ShyPerson's user avatar
  • 495
2 votes

Why Can't Mathematica Resolve this Simple Quantified Expression?

ContourPlot might help a little bit: ContourPlot[x^y == y^x, {x, 0, 2}, {y, 0, 2}, MaxRecursion -> 5,FrameLabel -> {x, y}] The only real solution(x>0,y>...
Ulrich Neumann's user avatar
2 votes

Proving an integral identity

Since we have $f(\sin(x))=f(\sin(\pi-x))$ for $0\leq x \leq \frac{\pi}{2}$ then we can rewrite $$\int_{0}^{\pi} x f(\sin(x)) d x=\int_{0}^{\frac{\pi}{2}} \left( x f(\sin(x)) + (\pi - x)f(\sin(x)) \...
Artes's user avatar
  • 57.3k
2 votes
Accepted

Implicit Function Theorem

First implicitly differentiate the expression with respect to x: $$\frac{d}{dx}\{e^{ax/y}+e^{bx/y}=c\}$$ We can do this in Mathematica: ...
Dominic's user avatar
  • 2,904
2 votes

How to deduce cosine theorem with vector?

Reduce can prove the cosine theorem but can not find the cosine theorem. ...
cvgmt's user avatar
  • 73.1k
1 vote
Accepted

Proving conjecture on number series

First off I have not found a pattern yet (update: look at edit 2, I have found a general pattern), just a simplification by setting some parameters to 0. It's not really what you asked for since I am ...
ydd's user avatar
  • 3,748
1 vote

Using the mathematical typography of formal logic

As mentioned by @CarlWoll in the comments, it comes down to the precedence of operators. ...
Domen's user avatar
  • 25.2k
1 vote
Accepted

How to deduce cosine theorem with vector?

...
xzczd's user avatar
  • 66.2k

Only top scored, non community-wiki answers of a minimum length are eligible