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