MathGroup Archive 2012

[Date Index] [Thread Index] [Author Index]

Search the Archive

Re: Mathematica Prove[...] Command Possible?

  • To: mathgroup at
  • Subject: [mg127998] Re: Mathematica Prove[...] Command Possible?
  • From: "Bill Simpson" <bsimpson141421356 at>
  • Date: Sat, 8 Sep 2012 03:07:08 -0400 (EDT)
  • Delivered-to:
  • Delivered-to:
  • Delivered-to:
  • Delivered-to:
  • References: <k1s9t5$ogb$> <k1v5pa$58n$> <k29m6u$aap$> <k2cd0f$f46$>

"amzoti" <amzoti at> wrote in message 
news:k2cd0f$f46$1 at
> On Thursday, September 6, 2012 1:18:41 AM UTC-7, magma wrote:
>> > > I have always been curious if Mathematica has ever considered a Prove 
>> > > command?
>> > See:
>> >
>> > Daniel
>> As Daniel just pointed out, Theorema is the package you are looking
>> for. It is in my opinion the BEST automatic theorem prover
>> available...anywhere. The new upcoming version 2.0 promises to be
>> spectacular! The current version 1.6 only works with Mathematica up to 
>> version
>> 7. In addition to the link above, posted by Daniel, you can look also
>> at:
> Excellent, I am looking forward to seeing and using that!
> Will it be able to do all of these as well?
> Thanks ~A

That book, and related books and journal articles, are
describing a relatively powerful geometry theorem prover
based on the work of Wen-tsun Wu which is often called the
"China Prover." Google
   Wu "China Prover" to start to find the literature.
People in the theorem proving community were surprised and
impressed with the complexity of proofs that this prover
cound handle. I believe there was a journalarticle titled
"The Complete Method of Wu" tried to nail down all the last
details of this.

In the simplest form it depends on the user manually
translating a geometry hypothesis into a sequence of
algebraic equalities. The prover then calculates a sequence
of multivariate polynomial remainders from those equalities
and if the final remainder is zero then the conclusion is a
linear combination of the premises and theorem is proven.
The calculated coefficients of the linear combination give
precise conditions for which the theorem holds.

Decades ago Wu originally implemented this in Pascal. More
recently it is claimed that this was easily implemented in
another system, but I have never been able to find the code.

I have wanted to get my hands on a working version of this
prover for a long time. I suspect in the simplest form it
might only be a page or two of Mathematica. In a more
complete form there are issues of irreducibility that need
to be addressed, but in many cases this is simple and for
some proofs this does not arise at all.

In the original form of the prover it was perhaps tedious to
do the manual translation into the equalities. I have
thought that perhaps another page of Mathematica might be
enough to automate most of this. That translation is
relatively straighforward.

I keep meaning to try to implement the prover in Mathematica
but I never get to this. If anyone is aware of an
implementation or is up to writing a page or so of code to
do this then it would provide a very simple powerful
geometry theorem prover for Mathematica users.

  • Prev by Date: Re: Transforming/expanding a list
  • Next by Date: Re: Landau letter, Re: Mathematica as a New Approach...
  • Previous by thread: Re: Mathematica Prove[...] Command Possible?
  • Next by thread: Re: A problem with Manipulate