From: Adam P. Goucher <apgoucher@gmx.com> To: math-fun <math-fun@mailman.xmission.com> Sent: Friday, September 30, 2011 7:36 AM Subject: Re: [math-fun] psycho-history, etc
This may be a good time to put in another plug for something I've wished for for years.
I want every mathematical fact on Wikipedia to come complete with one or more proofs linked to it. Furthermore, as theorem-proving technology advances, I would like each proof to be machine-checkable.
Machines cannot check general mathematical proofs, due to Gödel's Incompleteness Theorem. Indeed, if they could, mathematicians would quickly be rendered obsolete, as a computer could soon perform a breadth-first search of proofs.
Sincerely,
Adam P. Goucher
_______________________________________________
Humans can check mathematical proofs, so machines should also be able to. Gödel'sIncompleteness Theorem asserts that there are propositions that cannot be proved within a given axiom system, but which are true in an interpretation that steps outside that axiom system. It is perfectly possible for a computer to generate a list in which any proof will eventually appear. Mathematicians are useful because they selectively prove theorems that are interesting to their readers. -- Gene