that statement saying "actually, dumping hundreds of brute-forced proofs does not help with the practice and advancement of mathematics" is exactly the line software devs should take, but programmer pop culture has always valued short term convenience over most other concerns, so here we are