For the 99% of all mathematicians statement: I should probably take that back, as I don't know what the curriculum for mathematicians looks like these days. Maybe it's all algebraic topology and category theory for them now.
Instead of mathematician, I mean: people who could potentially benefit from interactive theorem proving technology.
Instead of mathematician, I mean: people who could potentially benefit from interactive theorem proving technology.