While mathematics certainly appears to me to be more of a meritocracy than the sciences, it’s still the case that the notion of proof has changed over time—and continues to change (witness Coq and friends) --, as have standards of rigor and what counts as mathematics. There are social and other non-mathematical reasons that influence how and why some ideas are accepted while others are rejected only to be accepted later, and vice versa.
It’s an interesting question whether this will always be the case or if it will converge on something approaching unanimously accepted truth and aesthetic criteria. Personally, I think mathematics is intrinsically an artistic endeavor and that the aesthetic aspect of it will never disappear. And where there is aesthetics, there is also politics and other sausage-making activities...
While mathematics certainly appears to me to be more of a meritocracy than the sciences, it’s still the case that the notion of proof has changed over time—and continues to change (witness Coq and friends) --, as have standards of rigor and what counts as mathematics.
The gold standard of what is a proof and what is not was achieved with the first-order predicate calculus a century ago and has not changed since. Leibniz’ dream has been realised in this area. However, no-one troubles to explicitly use the perfect language of mathematical proof and nothing else, except when the act of doing so is the point. It is enough to be able to speak it, and thereafter to use its idioms to the extent necessary to clearly communicate one’s ideas.
On the other hand, what proofs or theorems mathematicians find important or interesting will always be changing.
I don’t really think the question is whether mathematics is more meritocratic—it’s an economic question of credentialing. You need credentialing when you cannot cheaply verify performance. If I had a personal LHC and wrote a paper based on its results, I don’t think anyone would care too much about whether I have 2 PhDs or just a GED—the particle physicists would accept it. But of course, nobody has a personal LHC.
With mathematics, with formal machine-checkable proofs, the cost of verification is about as low as possible. How long does it take to load a Coq proof and check it? A second or two? Then all someone needs to do is take a look at my few premises; either the premises are dodgy (which should be obvious), or they’re common & acceptable (in which case they know I’m a math genius), or I’m exploiting a Coq flaw (in which case I’m also a math genius). Once they rule out #1, I’m golden and can begin turning the genie’s gift to good account.
By meritocracy, I meant what you explain by credentialing: the idea that the work alone is absolutely sufficient to establish itself as genius or crackpottery or obvious or uninteresting or whatever, that who you are, who you know, where you went to school and who your advisors were, which conferences you’ve presented at, the time and culture in which you find yourself, whether you’re working in a trendy sub-discipline, etc., that all that is irrelevant.
How much of mathematics is machine-checkable now? My (possibly mistaken) understanding was that even the optimists didn’t expect most of existing mathematics for decades at least. And how will we formalize the new branches of mathematics that have yet to be invented? They won’t spring forth fully formed as Coq proofs. Instead, they’ll be established person-to-person at the whiteboard, explained in coffee shops and over chinese food in between workshop sessions. And much, much later, somebody will formalize the radically revised descendant of the original proof, when the cutting edge has moved on.
I’ll know you’re right and I’m wrong if I ever begin to hear regular announcements of important new theorems being given in machine-checkable format by unaffiliated non-professionals and their being lauded quickly by the professionals. And that is the easier task, since it is the creation of new branches and the abstraction and merging of seemingly unrelated or only distantly related branches that is the heart of mathematics, and that seems even less likely to be able to be submitted to a theorem prover in the foreseeable future.
I’m not sure how one would measure that. The Metamath project claims over 8k proofs, starting with ZFC set theory. I would guess that has formalized quite a bit.
I’ll know you’re right and I’m wrong if I ever begin to hear regular announcements of important new theorems being given in machine-checkable format by unaffiliated non-professionals and their being lauded quickly by the professionals.
I think that only follows if genius outsiders really do need to break into mathematics. Most math is at the point where outsiders can’t do Fields-level work without becoming in the process insiders. Consider Perelman with Poincare’s conjecture—he sounds like an outsider, but if you look at his biography he was an insider (even just through his mother!).
While mathematics certainly appears to me to be more of a meritocracy than the sciences, it’s still the case that the notion of proof has changed over time—and continues to change (witness Coq and friends) --, as have standards of rigor and what counts as mathematics. There are social and other non-mathematical reasons that influence how and why some ideas are accepted while others are rejected only to be accepted later, and vice versa.
It’s an interesting question whether this will always be the case or if it will converge on something approaching unanimously accepted truth and aesthetic criteria. Personally, I think mathematics is intrinsically an artistic endeavor and that the aesthetic aspect of it will never disappear. And where there is aesthetics, there is also politics and other sausage-making activities...
The gold standard of what is a proof and what is not was achieved with the first-order predicate calculus a century ago and has not changed since. Leibniz’ dream has been realised in this area. However, no-one troubles to explicitly use the perfect language of mathematical proof and nothing else, except when the act of doing so is the point. It is enough to be able to speak it, and thereafter to use its idioms to the extent necessary to clearly communicate one’s ideas.
On the other hand, what proofs or theorems mathematicians find important or interesting will always be changing.
I don’t really think the question is whether mathematics is more meritocratic—it’s an economic question of credentialing. You need credentialing when you cannot cheaply verify performance. If I had a personal LHC and wrote a paper based on its results, I don’t think anyone would care too much about whether I have 2 PhDs or just a GED—the particle physicists would accept it. But of course, nobody has a personal LHC.
With mathematics, with formal machine-checkable proofs, the cost of verification is about as low as possible. How long does it take to load a Coq proof and check it? A second or two? Then all someone needs to do is take a look at my few premises; either the premises are dodgy (which should be obvious), or they’re common & acceptable (in which case they know I’m a math genius), or I’m exploiting a Coq flaw (in which case I’m also a math genius). Once they rule out #1, I’m golden and can begin turning the genie’s gift to good account.
By meritocracy, I meant what you explain by credentialing: the idea that the work alone is absolutely sufficient to establish itself as genius or crackpottery or obvious or uninteresting or whatever, that who you are, who you know, where you went to school and who your advisors were, which conferences you’ve presented at, the time and culture in which you find yourself, whether you’re working in a trendy sub-discipline, etc., that all that is irrelevant.
How much of mathematics is machine-checkable now? My (possibly mistaken) understanding was that even the optimists didn’t expect most of existing mathematics for decades at least. And how will we formalize the new branches of mathematics that have yet to be invented? They won’t spring forth fully formed as Coq proofs. Instead, they’ll be established person-to-person at the whiteboard, explained in coffee shops and over chinese food in between workshop sessions. And much, much later, somebody will formalize the radically revised descendant of the original proof, when the cutting edge has moved on.
I’ll know you’re right and I’m wrong if I ever begin to hear regular announcements of important new theorems being given in machine-checkable format by unaffiliated non-professionals and their being lauded quickly by the professionals. And that is the easier task, since it is the creation of new branches and the abstraction and merging of seemingly unrelated or only distantly related branches that is the heart of mathematics, and that seems even less likely to be able to be submitted to a theorem prover in the foreseeable future.
I’m not sure how one would measure that. The Metamath project claims over 8k proofs, starting with ZFC set theory. I would guess that has formalized quite a bit.
I think that only follows if genius outsiders really do need to break into mathematics. Most math is at the point where outsiders can’t do Fields-level work without becoming in the process insiders. Consider Perelman with Poincare’s conjecture—he sounds like an outsider, but if you look at his biography he was an insider (even just through his mother!).