Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » Software » comp.soft-sys.math.mathematica

Topic: Command Possible?
Replies: 3   Last Post: Sep 6, 2012 4:13 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Ralph Dratman

Posts: 62
Registered: 5/13/11
Re: Command Possible?
Posted: Sep 3, 2012 3:01 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply


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@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.
>
>
>





Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.