Agree, but more specifically Math is clearly about a human understanding structure of things. Math is basically for humans. It's one of the main reasons understandable proof is so important.
replyWell, by "understanding" I mean "understanding by humans", indeed.
replyEngineering is used fairly loosely these days but I insist engineering ends where you have to prove theorems.
replyThat’s a strange delineation. Engineering is essentially about designing a thing, asking whether that thing really does satisfy the desired criteria, and then iterating when it does not. Mathematical models of the world are tremendously useful to this practice—engineers don’t need to guess about many aspect of the real world: they have physics. What they want, more than anything else, is strong evidence that a property holds. Internal validity (proof) and external validity (experiment) are the best evidence that you can get—why would you throw one of those approaches away?
replySo what I’m most curious about is this: if there are axioms and proofs so enormous that a human could never prove them in a lifetime, but a machine can, does that make it engineering? That’s the point I’m really wondering about.
replyI mean, what if a human could follow every single step of the process in principle, but the sheer volume is so vast that a human can never see the whole thing—would that be engineering?
But I don’t think of that as engineering. In the future, maybe it will be called an Oracle
I would call it "Engineered (as machine-made trustworthy) Mathematics": you have results but nobody undrstands them but they were not produced by humans.
replyDespite that, people use them. In that sense, similar to the Finite Elements method. But the tools (statements) are machined like any other tool (screwdriver).
Similar to microprocessors in your example. But about statements.
You might have gotten it backwards. Proofs are essentially rooted trees
replyThe details could be painful but having a birds eye view is always possible?
And having a machine compress it for human consumption, sounds very plausible (and which I think of as engineering)