3 ms·
Errors are common in mathematics in practice, though, and even expected to a degree because errors in a deep theorem or proof can be extremely subtle. A complex
by gh02t 8y ago
Errors are common in mathematics in practice, though, and even expected to a degree because errors in a deep theorem or proof can be extremely subtle. A complex monograph might contain dozens of proofs and lemmas, all of which are completely interdependent so one mistake can be a major problem requiring significant revisions.
Part of the purpose for publishing in the first place is to see if other people can find mistakes in your logic. This is particularly the case at the real frontiers of science and theoretical mathematics, where truly new ground is being broken. Computer-aided theorem provers would like to improve this, but they are currently fairly specialized tools with limited use.
- User23 8y agoThere are certainly some examples. However a lot of older mathematics was actually quite sloppy formally speaking. It was the demands of early primitive and unreliable computing hardware that forced developers to focus on provable software correctness: it was the best way to find hardware bugs! Dijkstra has a great monograph on developing early interrupt handling correctly. More people should read it, since as anyone who has worked with Unix signals knows, it's easy to get wrong in subtle and nasty ways. Edit: Also to speak to the pure math point, Dijkstra's official title after graduating was "Mathematical Engineer."
- gh02t 8y agoI'm aware, but I'm more talking about theoretical computer science than practical software and systems engineering. Methods for formal verification and design of software are of course interesting, but quite different from formal verification of theory. What I wanted to point out is that even a very formal field (advanced, pure math) is still plagued by very mundane and very human logical errors. Further, these errors are not easily spotted by machine, at least not with current technology. Regarding Dijkstra, I personally consider TCS to be a branch of applied math or maybe applied logic. What most programmers do in practice, however, is more akin to engineering (or I'd say, is a type of engineering).