# Tag Info

## Hot answers tagged proof

24

After all this time, I came up with a very nice tensor calculus proof of the Hairy Ball Theorem. It only depends on Stokes theorem and standard laws of tensor calculus like the Ricci identity and symmetries of curvature tensors. All the topology is done by Stokes theorem. The remainder of the proof is equational, local and geometrical. It is coordinate/basis ...

21

As far as obtaining a True/False answer: Element[Sqrt[2], Rationals] (* False *)

17

f[n_] := (n (n + 1) (2 n + 1))/6 Easy. The proof by induction involves two steps: Prove the relation for a starting value. We'll take n=1. So f[1] must equal 1^2: f[1] == 1 True Prove that, if the relation holds for a certain n, it also holds for n+1. In this case, for n+1 we have to add (n+1)^2 to the sum you get for n: f[n] + (n + 1)^2 == f[n + 1]//...

15

At first we should try to envision what kind of function it might be. We need no computer system for that. So let's start with assumptons: $f$ is a real valued function on the real domain. Therefore we have: $$f(x+0)^2=f(x)^2+f(0)^2$$ thus $$f(0)=0$$ Then $$f(x-x)^2=f(x)^2+f(-x)^2$$ it implies $$0=f(x)^2+f(-x)^2$$ Sum of two non-negative numbers is zero (...

13

One can simply use: Limit[((1 + a x)^(1/4) - (1 + b x)^(1/4))/x, x -> 0] to get the result. However Limit does know about the l'Hopital rule. Nonetheless there are different ways to go, e.g. let's use Series to write down the first few terms of the Taylor series of ((1 + a x)^(1/4) - (1 + b x)^(1/4))/x: Series[((1 + a x)^(1/4) - (1 + b x)^(1/4))/x, {x,...

12

We needn't guess many (thousands) cases in order to verify the underlying statement if we harness some handy Mathematica functions like CountRoots, RegionPlot3D or Manipulate. At first, we can observe that, the equation can be easily transformed to a polynomial type by an appropriate multiplication (applying Expand on the left hand side of the equation we ...

12

If FindInstance[ expr, vars, dom] returns no instances - {}, it does not mean (in general) there are no solutions, i.e. it does not prove anything here. Some kind of reasonable arguments you can get making use of Reduce, if you change the head of FindInstance[ expr, vars, dom] into Reduce[ expr, vars, dom] and evaluate it, that will return False. However ...

12

How about FullSimplify[ Exists[{a, b}, Element[a, Integers] && Element[b, Integers] && ! MemberQ[Divisors[b], a] && a^2/b^2 == 2]] (* False *)

11

Let's define the function f suitably: f[x_, a_, b_] := Log[x, 1 + (x^a - 1)*(x^b - 1)/(x - 1)] We would have defined f with appropriate conditions (I recommend to examine this post: Placement of Condition /; expressions), e.g. f[x_, a_, b_] /; 0 < a < 1 && 0 < b < 1 && x > 0 := ... however since we are to deal with ...

11

For proving statements like this you can enter predicate logic quantifiers directly into Mathematica and let it try to Resolve the formula to a truth value. First we state the problem ingredients ω = FullSimplify[ π-4 ArcCos[1/3]+2 ArcCos[(2 (1/2+1/8 (-1-3 Cos[4 ArcCos[1/3]]))) / Sqrt[3 (1-1/16 (1+3 Cos[4 ArcCos[1/3]])^2)]] ] vars = {a,b,...

10

Applying the experimental method, we can see that the conjecture is false. Let {\[CapitalSigma], g, b} = {-8.12029, 4.79026, 1.46801} Then solve for the roots: NSolve[1 - (b/r)^2 - g^-2*(2/15*\[CapitalSigma]^9 (1/(r - 1)^9 - 1/(r + 1)^9 - 9/(8 r) (1/(r - 1)^8 - 1/(r + 1)^8)) - \[CapitalSigma]^3 (1/(r - 1)^3 - 1/(r + 1)^3 - 3/(2 r) (1/(r - 1)^...

9

Induction has many faces, a straightforward way to prove the equality using induction is 1. RSolve It is superior because we needn't know the formula. Denote s[n] to be the sum 1^2 + 2^2 +...+ n^2 for every natural n, then obviously the axiom of induction is equivalent to : s[n+1] - s[n] == (n+1)^2, and the initial condition is : s[0] == 0, thus : RSolve[{...

8

Since Reduce doesn't seem to like the inequality, I tried FullSimplify with Assumptions instead. This works in three steps: differenceByTerm = SeriesCoefficient[(1 + x)^n - (1 + n x), {x, 0, m}] $$\cases{ 0 & m=0 \\ \binom{n}{m} & m>1 \\ 0 & \text{True} \\ }$$ FullSimplify[ differenceByTerm >= 0, Assumptions -> n > 1 ...

8

Integration by parts gives $$\int_0^1 x^k \sin(\pi x) dx = \frac{1}{\pi} + \frac{k}{\pi}\int_0^1 x^{k-1} \cos(\pi x) dx$$ and $$\int_0^1 x^k \cos(\pi x) dx = - \frac{k}{\pi}\int_0^1 x^{k-1} \sin(\pi x) dx.$$ Applying these rules in succession to $j_{n+1}$ immediately gives $$j_{n+1} = \frac{1}{\pi} - \frac{(2n+1)(2n+2)}{\pi^2} j_n$$ which clearly is ...

8

Even though Mathematica has a broad range of powerful capabilites (see e.g. this comparison of computer algebra systems) in related fields (number theory, quantifier elimination) it sometimes doesn't appear to be clever enough to prove simple theorems, e.g. this should yield False however we get back the input: Resolve[ Exists[p, p ∈ Integers && ...

7

Yes, Mathematica can prove these inequalities symbolically. To be more precise, it can Reduce them to True. Generating human-readable proofs is also possible but that's one broad topic. First, we'll use a “coordinate change”. Notice that your expressions for R, s, r are all symmetric in x, y, z. This hints that we might benefit from using symmetric ...

7

First, let us notice that the limit follows from the following: Lemma. $\displaystyle \lim_{u \rightarrow 0} {(1+u)^{1/4}-1 \over u} = {1 \over 4}$. For $${{(1+a\,x)^{1/4} - (1+b\,x)^{1/4}} \over {x}} = {{(1+a\,x)^{1/4} - 1} \over {x}} - {{(1+b\,x)^{1/4} - 1} \over {x}}$$ $$= a\,{{(1+u)^{1/4} - 1} \over {u}} - b\,{{(1+v)^{1/4} - 1} \over {v}}\,,$$ ...

7

You don't need FindEquationalProof to this end, it is enough to use the quantifiers. ForAll[{a, b, c}, Implies[Implies[a, b] && Implies[b, c], Implies[a, c]]]; Resolve[%] True See Mathematica help for more info. If you insist to use FindEquationalProof here, then you may apply the following axioms of propositional logic shefferLogic = {ForAll[a,...

6

The quickest route here, from a syntactic standpoint, is to use Reduce, which allows you to request that the equation to be simplified by eliminating a set of variables, and to restrict those variables to a given domain, all at once: In[1]:= Reduce[a^2/b^2 == 2, {a, b}, Integers] Out[1]= False As shown in Marius Ladegård Meyer's answer, you need to square ...

6

We can use Reduce to give us: expr = (2^p - (2^2) (3^2))/(3^3); Reduce[{expr == n, n ∈ Integers}, p, Integers] (n | p) ∈ Integers && n >= -1 && p == Log2[9 (4 + 3 n)] Since the only x such that Log2[x] ∈ Integers are powers of two, we must have 9 (4 + 3 n) equal a power of two while n is simultaneously an integer. This clearly cannot ...

6

Can you do the following: Trace[FullSimplify[expr], TraceInternal -> True] or FullSimplify[expr, TransformationFunctions -> {Sow, Automatic}] // Reap References: What are the default TransformationFunctions used in Simplify and FullSimplify? Simplify with TransformationFunctions, Bug? http://12000.org/my_notes/faq/mma_notes/MMA.htm#x1-1600015 http://...

6

Define DiracMatrix: DiracMatrix[k_] /; k == 1 || k == 2 || k == 3 := ArrayFlatten[{{0, - I PauliMatrix[k]}, {I PauliMatrix[k], 0}}] DiracMatrix[4] := ArrayFlatten[{{ IdentityMatrix[2], 0}, {0, -IdentityMatrix[2]}}] DiracMatrix[5] := Dot @@ Table[DiracMatrix[k], {k, 4}] To prove the identity we could check e.g. And @@ Flatten @ Table[ DiracMatrix[i]....

6

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 the question, Murray's command for proving that the right identity is unique: FindEquationalProof[Implies[ForAll[a, g[a, f]==a], e==f], groupTheory ] fails with a message that there is an invalid ...

5

I think that there is a fundamental misunderstanding here. In Mathematica certain expressions are meant to represent mathematica statements. x > 1 is an example of this. Other expressions are simply program code, which is run by the system, like in any other programming language. An example is Table[x, {x,10}]. Sometimes there is a level of overlap ...

4

Just a small remark: if the variables are angles then you should probably make the bounds periodic, using something like Mod[a, 2 Pi] instead of a in the conditions. Then you obviously get solutions to this trivial problem. Here I just did it for one of the variables: FindInstance[ a + b + c + d + e + f + g + h + i == 16 Pi - 33 ArcCos[1/3] - \[Omega] &...

4

This solution gets a trivial step away from the answer. (Strikeout after addressing the comments.) You can consider the difference diff = int - intpaper, and check that it vanishes. Rather than having Mathematica take the imaginary part, do it "by hand": intpaperz = 2/Sqrt[-1 - (Sqrt[-1 + Sqrt[3]] l - 2 I \[Tau])^2/(3 + Sqrt[3])]; intpaperzc = 2/Sqrt[-1 ...

4

A very quick, brute force way: With[{partitions = IntegerPartitions[49, {5}]}, Pick[partitions, Times @@@ partitions, 13000] ] {{25, 13, 5, 4, 2}, {20, 13, 10, 5, 1}}

4

Is it acceptable to use this result as part of the formal proof of my proposition? In general, no... Mathematica has bugs and problems with differences between its interpretation of things vs. what users may expect. A better approach would be to post the equations or describe them to see what form they take and find out if anyone knows a way to prove they'...

4

Mathematica typically works with complex numbers. It turns out however that the identity $a^n b^n = \left(a b\right)^n$ is not generally true for all complex numbers. This can be quickly verified with FindInstance: FindInstance[(a b)^n != a^n b^n, {a, b, n}] The two major conditions this will be true is if $n \in \mathbb{Z}$ or if $a>0 \land b>0$. ...

4

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 to it as arguments in FindEquationalProof. So Mathematica probably crashed when presented with unbound variables. Second, FindEquationalProof requires a full ...

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