ARR! statistics about .. well, mathematics.

i like the way this guy thinks:

"... 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 mathematics 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)

reading this reminds me also of the flysρeck project, regarding the use of formal proof:as expounded on their wiki:

" 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, all the 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."

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.

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 witness how it does ..

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

going 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).

ye gods: that would be a really complicated network!