> There is a similar disaster inbound for mathematicians. Formal mathematics is tedious and mostly only shows things that you were pretty sure were true anyway, so why bother.
> It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.
Formalized mathematics is just a very small subset of what mathematicians work on: in my observation people who work on (computer) formalized proofs often rather sit in CS departments.
> It turns out the physicists and engineers have unsportingly built machines which are really, really good at the tedious bookwork required by formal mathematics. That is going to go exactly the same way that introducing measurement to philosophy went for the philosophers.
Formalized mathematics is just a very small subset of what mathematicians work on: in my observation people who work on (computer) formalized proofs often rather sit in CS departments.