Re: Command Possible?

*To*: mathgroup at smc.vnet.net*Subject*: [mg127935] Re: Command Possible?*From*: Ralph Dratman <ralph.dratman at gmail.com>*Date*: Mon, 3 Sep 2012 02:56:09 -0400 (EDT)*Delivered-to*: l-mathgroup@mail-archive0.wolfram.com*Delivered-to*: l-mathgroup@wolfram.com*Delivered-to*: mathgroup-newout@smc.vnet.net*Delivered-to*: mathgroup-newsend@smc.vnet.net*References*: <20120901062806.D256E6872@smc.vnet.net>

It always seems to me that everything depends on what sort of proof you want. Mathematica doubtless knows how to classify the square root of a non-square integer as irrational, but I very much doubt it uses anything like the kind of logic people prefer to associate with elementary proofs of important ideas. Mathematica presumably takes advantage of a large number of accepted theorems. So the proof that the square root of 2 is irrational would likely amount to the use of a method which has, at some point in the past, directly or indirectly, been proved to properly classify various kinds of numbers as rational or irrational, as well as algebraic, transcendental, algorithmic or whatever other categories might be relevant to a particular task. I have read that Russell and Whitehead's Principia Mathematica occupies itself for a thousand pages to prove that 1+1=2 (see, eg., http://blog.plover.com/math/PM.html). Few people want to see a proof at that level of detail. Published proofs rely on the Peano axioms and some well-studied results to which they lead. Yet apparently it is not possible to prove that the axioms are consistent. That does not represent any sort of practical problem, but it supports the notion that in proving things, you have to decide where to call a halt. Doing so involves a set of aesthetic choices. You say you just want a proof, but actually you are asking the computer (or rather, the programmer) to produce a kind of artwork. The results are likely to disappoint. Ralph Dratman On Sat, Sep 1, 2012 at 2:28 AM, amzoti <amzoti at gmail.com> wrote: > Hello, > > I have always been curious if Mathematica has ever considered a Prove > command? > > The reason one could ask such is question is simple, who would have ever > thought that CASs would get to where they are in such a relatively short > period of time. > > Certainly, this is a tall order, but the richness we already see in > Mathematica leads one to believe that this can be a new area for CAS > development. > > Some easy examples could be Prove[ Sqrt[2], Irrational], Prove[ Exp[x], > Transcendental], Prove[Sum[i, {i, 1, n}]== n(n+1)/2]... > > Certainly, there would be many limitations with proofs in some branches of > Mathematics. I suppose getting to meatier proofs is problematic in itself, > but maybe a certain rigor in defining the problem can be mapped out that > follows how we set problems up today (as there is a pretty consistent way > to specifying problems that most mathematicians adhere to). > > Anyway, why has this not been attempted (as a comparison, I have seen like > DC Proof)? In the end, maybe it is just not a goal for a CAS. > > Thanks for your time. > > >

**References**:**Mathematica Prove[...] Command Possible?***From:*amzoti <amzoti@gmail.com>