i like the way this guy thinks:

i think this comparison also highlights their comparative advantages nicely:

ye gods: that would be a really complicated network!

"... but I think we're starting to see a new kind of metamathematics, where people use statistical methods to study the structure of mathematics itself. This is mathematicsreading this reminds me also of the flysρeck project, regarding the use of formal proof:as expounded on their wiki:as actually done by people, so it involves issues of taste and style. These are subjective things. But I suspect there are some features of math that are fairly independent of who is doing it. Maybe some theorems are 'important' in a fairly objective sense - important crossroads that most travelers tend to stop at. And someday we may understand why."

~ from "The network of mathematics" @johnbaez:g+ (via mathbabe)

"the way i understand it, traditional proofs are like pseudocode whereas formal proofs would be real computer programs that you can "compile" against the standard axioms .. although it would probably resemble machine code.How does a formal proof differ from a traditional mathematical proof?

Traditional mathematical proofs are written in a way to make them easily understood by mathematicians. Routine logical steps are omitted. An enormous amount of context is assumed on the part of the reader. Proofs, especially in topology and geometry, rely on intuitive arguments in situations where a trained mathematician would be capable of translating those intuitive arguments into a more rigorous argument.

In a formal proof,allthe intermediate logical steps are supplied. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors."

i think this comparison also highlights their comparative advantages nicely:

the formal proof mightn't be readable, but at least you know it runs and witnessgoing back to the idea of a network of all mathematics, i suppose that a formal proof would be checking the existence of a continuum from a statement (a given node on that network) to the fundamental axioms (or "roots" of the network).howit does ..

.. whereas getting the idea for the formal proof would probably require some basic principles forwhyit could conceivably work, in which case one would probably have a traditional proof in mind.

ye gods: that would be a really complicated network!

## No comments:

Post a Comment