How much of mathematics is machine-checkable now?

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