[chongli]

Asking working mathematicians to formalize their proofs in a machine-checkable system is like asking photographers to become electronics engineers so they can build their own digital cameras from scratch. It's not a reasonable request. It's so far outside of a typical mathematician's lane it's not even on the same continent.

[hgsgm]

They could do what every other scientist does, and pay people to build and run the tools they need to get scientifically valid results from their experiments.

[chongli]

Math isn’t science. Most mathematicians aren’t interested in applications to the real world. They don’t care about empiricism or validity. The fact that a lot of applications have come out of math is a side effect.

Imagine if someone discovered a way to solve real world problems by formulating them as chess positions. Would it be reasonable of us to demand that chess players stop competing and work on these formulations? No, and I don’t think many chess players would jump at the opportunity. They just want to play chess!