Re: Deep Thoughts # 7: A New Kind of Mathematics

From: Vlad (vtt0000_at_mail.utexas.edu)
Date: 06/25/04 

Date: Fri, 25 Jun 2004 14:28:46 -0500

Charlie-Boo wrote:

>Vlad <vtt0000@mail.utexas.edu> wrote
>
>
>
>>This is exactly my feeling about this. I do not understand why
>>is deriving properties of a program more elegant, than formalizing
>>directly an untiuitve notion which we can describe informaly
>>in some natural language (or only have as an idea in our mind).
>>
>>
>
>
>
>>Vladimir Trifonov
>>
>>
>
>I thought about your comments, and it perhaps helped me appreciate
>even more what it means to express something as a (computer) program.
>
><snip>
>
>The power of the computer to make us infinitely more skilled in task #
>1 is clear and has been thoroughly exploited by our society. Task # 2
>has been optimized to a lesser degree. What I am referring to is
>harnessing the power of the computer and applying it to # 3 - many
>more novel problems of mathematics, logic, computability, complexity,
>geometry, essentially every branch of mathematics and computer
>science.
>
>Charlie Volkstorf
>Cambridge, MA
>
>
This all is very nice, but it is by far not "A New Kind of Mathematics".
Research
on automatic theorem proving and verification has existed for many
years. In fact
the work of Boyer and Moore that you mention in another post is exactlly
along those lines. It is ironic that you mention their work, because
what you claim to
be inventing they have been working on for 20 years. In that post you
ask what is the
relative merit of theorem proving and your generation of axioms from a
program.
The merit of both is large. The real question is about their
feasibility. Verifying a
proof is feasible, although a daunting task, because to verify the
proof of any
substantial mathematical result, you have to develop a huge database of
definitions
and theorems (e.g. see Mizar project). This is the merit of the result
of B&M --
they actually formalized enough math (in something that looks like
program in Lisp,
i.e. exactly what you claim to be inventing) and verified a substantial
result in
mathematics. Automatically proving a theorem is by far not as feasible
as verification
(and if you believe that P<>NP, it might be even infeasible). Your are
talking about
not only automatically proving a theorem, but also automatically
generating its
statement (or as you call it -- automatic axiom generation). This to me
is outright
infeasible (at least not on a Turing Machine). For example althoug you
can probably
systematically generate all properties of a program, how would you know
which
ones are interesting and when are they going to happen.

You compare your work with the work of Boyer and Moore. Do not. Maybe
when you can actually provide eiher explicitly or on demand a back up of
your
statements (something which Boyer and Moore will certainly do, if you
ask them
politely), can you claim that there is an asymetry between your proposal and
their work. My advice to you is to sit down and do a lot of dirty work
before
you come out and say you have _invented_ something new that will
revolutionize
the world as we know it. Vague and unsubsantiated statements that sound
good,
do not prove anything and belong more to the world of fiction than to
the world of science. And your proposal at the moment is science
fiction. I do
not doubt the usefulness of computers for proving new and interesting
mathematical results (see proof of Four Color Theorem), but your claim
that you
came up with this idea and your ability to back up your statements with
actual
results.

Vladimir Trifonov

Relevant Pages

  • Re: Deep Thoughts # 7: A New Kind of Mathematics
    ... >>is deriving properties of a program more elegant, than formalizing ... >more novel problems of mathematics, logic, computability, complexity, ... on automatic theorem proving and verification has existed for many ...
    (sci.logic)
  • Re: Another Reason Why Collatz is Unprovable
    ... going to produce anything surprising, ... When one takes mathematics to a higher ... predict counterexamples without running the algorithm itself. ... Proving that there can't exist ...
    (sci.math)
  • Re: What is a proof, exactly?
    ... Because that's what proving things is all about. ... proof - I'm trying to get to know what that standard looks like. ... there is a formal proof, being a sequence of statements following from ... be possible to actually have a foundation for mathematics based purely on ...
    (sci.math)
  • Re: Why?
    ... as "the mathematics needed to to do applied science". ... the Bishop and Bridges book does not give a formal theory. ... learn more I can take a stab at formalizing it myself. ...
    (sci.logic)
  • Re: How do We Know that ZF is the Axiomatization that Proves everything Provable?
    ... of a large number of branches of mathematics can be developed. ... matter of ZFC formalizing mathematics. ... Who EVER said that ZFC contains "all the principles of logic"? ... than ZFC to capture ordinary mathematics. ...
    (sci.logic)