Re: [math-fun] Proof (was: Missing Catalan identity)

On 6/14/08, Steve Witham <sw@tiac.net> wrote:

...

James Buddenhagen wrote:

. . . something that has been bothering me for a long time: when should I accept that something is true? ... Nobody mentioned truly formalizing math and using proof- checking programs. Doing that would break the problem down. ...

There was some discussion of this on math-fun a year or so ago ... Certainly, there are plenty of people working on it. One example is the Hilbert II project at www.qedeq.org/ WFL