[FOM] Gap in the original Hales-Ferguson proof of Kepler

[roux cody]

>
> But suppose that the proof assistant had been a lot more "intelligent"
> than today's proof assistants are, and had *figured out on its own how to
> plug the gap*.  Then we humans might never have become aware that there was
> a subtle point that had been overlooked.  The critics would then have been
> at least partially vindicated: The machinery of formal proofs would have
> stolen away an opportunity for deeper understanding.
>
>
This seems like a strange hypothetical, since as others have pointed out,
proof assistants still stumble on tiny baby steps. But a world in which
these steps could be made automatically would be truly a wonderful one in
my opinion, in which mathematicians could jump from insight to insight and
from lemma to proof, trying out new and crazy ideas relying on the machine
to weed out the silly ones. Just as we don't need to worry about computing
the product of 6 digit integers, we would be able to give up this silly
"detail checking" business. Maybe it's just me though.

One area were I really would be reassured by automated deduction would be
category theory, where it seems that every lemma is proven "by an easy
diagram chase" without much insight to be gained except by an unexpected
mistake.

I would also be happy to welcome our computerized overlords, if they would
only hurry to show up!

Best,
Cody




> Admittedly, in this case, even if a proof assistant had plugged the gap,
> the "lost insight" would not have been a big loss to mathematics.  After
> all, the argument amounted to showing that a certain weird situation was
> not a real possibility, so who really cares?  As proof assistants become
> more intelligent, however, perhaps their ability to fill gaps in reasoning
> could "hide" bigger and bigger insights.
>
> In one sense, this issue is not new.  There is already a danger that we
> could become over-reliant on Groebner basis algorithms and miss geometric
> insights, or over-reliant on WZ-style identity provers and miss
> combinatorial insights.  Atiyah is reported to have said: "Algebra is the
> offer made by the devil to the mathematician.  The devil says: `I will give
> you this powerful machine; it will answer any question you like. All you
> need to do is give me your soul: give up geometry and you will have this
> marvellous machine.'"  Still, proof assistants potentially take this
> Faustian bargain up to a new level.  I, for one, would still welcome our
> new theorem-proving overlords, but with more sympathy for the critics that
> I previously dismissed.
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151231/48982219/attachment-0001.html>