What he described is less ambitious than Hilbert's Program.

He just wanted to have computers (which hopefully are less fallible than humans) systematically verify known mathematics. While I see this as interesting to attempt, it is also doomed to fail because more math is being produced faster than you can possibly verify it.

Which brings up a dirty little secret of mathematics. You can consider a mathematical proof as being like a computer program that has been specced out in detail, but never run. Yeah, you think that it would work. But if you tried to implement it you'd run into little roadblocks. Most of them you could get around. But you never have any idea what is lurking in there, and no real way to find out.

And no, this is not a trivial problem. In fact entire areas of mathematics have fallen apart because problems were found, and found to be serious. My current favorite example is the classification of finite groups. Nobody has really reviewed the proof. Everyone knows that the proof has flaws. And the situation is serious enough that there is a decades-long effort under way to find a different proof of the result! (The effort was started by some of the people who made their reputation working on the original proof.)

In reply to Re^3: What do you know, and how do you know that you know it? by tilly
in thread What do you know, and how do you know that you know it? by tilly

Use:  <p> text here (a paragraph) </p>
and:  <code> code here </code>
to format your post; it's "PerlMonks-approved HTML":

  • Posts are HTML formatted. Put <p> </p> tags around your paragraphs. Put <code> </code> tags around your code and data!
  • Titles consisting of a single word are discouraged, and in most cases are disallowed outright.
  • Read Where should I post X? if you're not absolutely sure you're posting in the right place.
  • Please read these before you post! —
  • Posts may use any of the Perl Monks Approved HTML tags:
    a, abbr, b, big, blockquote, br, caption, center, col, colgroup, dd, del, div, dl, dt, em, font, h1, h2, h3, h4, h5, h6, hr, i, ins, li, ol, p, pre, readmore, small, span, spoiler, strike, strong, sub, sup, table, tbody, td, tfoot, th, thead, tr, tt, u, ul, wbr
  • You may need to use entities for some characters, as follows. (Exception: Within code tags, you can put the characters literally.)
            For:     Use:
    & &amp;
    < &lt;
    > &gt;
    [ &#91;
    ] &#93;
  • Link using PerlMonks shortcuts! What shortcuts can I use for linking?
  • See Writeup Formatting Tips and other pages linked from there for more info.