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