On: Knuth: Computer Programming as an Art

[fburnaby]

I like to think of it as Hofstadter suggests; theorem proving is mechanical, but there is a very beautiful art in selection of the axioms.

[nearestneighbor → fburnaby]

In some idealized form of math, proving theorems is indeed mechanical, but the branching factor is extremely high.

[gruseom → fburnaby]

I like to think of it as Hofstadter suggests; theorem proving is mechanical

Does he really say that? If so, he must not have proven any. Few things require more imagination.

[RiderOfGiraffes → fburnaby]

That's just wrong. Hofstadter never says that theorem proving is mechanical, and if he did, he'd be wrong.

Demonstrating a proof can be mechanical, which is why proof assistants such as Coq can work, but finding a proof, that's an art.

[10ren → fburnaby]

It is by logic we prove, it is by intuition that we invent. - henri poincaré

http://www-history.mcs.st-and.ac.uk/Biographies/Poincare.htm...

[christopherolah → fburnaby]

>theorem proving is mechanical

I have to disagree. As theorems become more complicated, proving them becomes anything but mechanical: one must choose between an infinite variety of approaches, many of which are equally valid.