Comment by JonChesterfield

> On formal mathematics, almost no mathematicians pay attention to this afaik. It's something that lives in philosophy departments, not mathematics.

In the old days there were philosophers. They sought truth through thought and wisdom. Some started to measure reality and compare thought against that measurement, but real philosophers paid little heed for it didn't matter.

Testing their theory became known as physics. It turned out the testing against reality can be used without the theory, which we call engineering. We still have philosophers and they still pay little heed to measurement.

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.