Re: Complete Arithmetic?

From: David C. Ullrich (ullrich_at_math.okstate.edu)
Date: 01/03/05 

Date: Mon, 03 Jan 2005 13:59:31 -0600

On Mon, 03 Jan 2005 15:14:36 +0100, Steven <steven2000@despammed.com>
wrote:

>> (Some computer guys down the hall have some thoughts
>> that seem quite far-fetched to me about using
>> "genetic programming" to solve some unsolved problem
>> in mathematics. They were planning on going for
>> Fermat's Last Theorem until I told them that that
>> had been done...)
>Building automated theorem prover is a great challenge, and much research
>has been done here, but still the abilities are way beyond expectations.
>The more interesting axiom systems are not complete, but this is not such a
>big problem; rather the computational complexity is. Going for Fermat's
>theorem seems very naive, if you consider the abilities of todays automated
>theorem prover... they usually fail with theorems that can be shown by
>schoolkids.
>Genetic programming can be regarded as a buzzword. There are rumours about
>very successful applications of that approach, but I think they are
>obtained with "Core Wars", an assembly language game with about 10
>commands.
>Theorem provers are useful to verify formal proofs, and to do a lot of
>rather trivial proving; but it still requires a human to do math.

In case it wasn't clear, that all seems perfectly correct to me - I
told the guys as much, (except for the bit about genetic programming
being a buzzword), but they've been very successful in using genetic
programming to play blackjack and so they're determined to move
on to unsolved mathematics...

>Have fun!
>

************************

David C. Ullrich

Relevant Pages

  • Re: ZFC
    ... >>I got into the subject by writing on a theorem prover, ... > To say that the foundations of mathematics are unclear suggests that the ... attained automated induction proofs, done via a breadth first search, so ...
    (comp.theory)
  • Re: ZFC
    ... >I got into the subject by writing on a theorem prover, ... To say that the foundations of mathematics are unclear suggests that the ... mean that there's anything logically suspect about ZFC. ...
    (comp.theory)
  • Re: Complete Arithmetic?
    ... They were planning on going for ... Building automated theorem prover is a great challenge, ... but still the abilities are way beyond expectations. ...
    (sci.logic)
  • Re: the error in Godels proof
    ... tell us more about this theorem prover. ... Moving mathematics forward is exactly why Godel's ... to calculation, ... Theorem with your own standard of usefulness, ...
    (sci.math)