> You're jumping around a bit.
In that case, anyone who uses more than one example to make his point is jumping around. If allowed to prevail, this non-argument would cripple debate.
> Did the four-color map problem use numerical results?
Yes, emphatically so. There were a certain finite number of possible maps (1936 to be precise), and each of them had to be tested explicitly. The reason for the requirement for full disclosure was that the tested set needed to be examined to assure that nothing germane was excluded, nothing included on specious grounds, and the manner of testing had to be closely examined. None of this could be reduced to a simple equation, and none of it yielded to a formal, concise mathematical proof.
> I imagine it was just a pure combinatorial enumeration problem (I have not read the original paper, I may be wrong about that).
If that were true, there would have been no role for a computer program -- it would have been published as a pure and formal result, like Fermat's last theorem. No one would have cared about the role played by computers, because a formal and pure proof could be examined by anyone sufficiently versed in mathematics.
> What kinds of actual fields of mathematics are you thinking about, here?
Any field that would benefit from use of a computer. By recent count, that's nearly all mathematical fields for one reason or another, including areas we once might have thought would have no use for a computer. Computer mathematics has gotten to the point where computers, laboring independently, come up with new theorems that humans have overlooked.
> I know that error analysis is a deep and arcane subject, and personally I have no idea how well or badly we do in that department, but I'm struggling to think of where the details of how we get it wrong or right is crucial for the development of published academic mathematics.
Most struggle with that, and part of the struggle is being able to see the detail of the algorithms used to arrive at a result. No detail, no trust, no science.
> "Most" maths is totally abstract these days ...
Not relevant. Relevant would be whether that abstract mathematics is or is not fully revealed in its details. For science, it must be.
This article --
http://www.newscientist.com/article/dn7286-computer-generate...
-- discusses the role of theorem-proving software like Coq, but includes a misleading statement by someone at Microsoft: "Microsoft hopes to develop a similar system for checking the logic used in computer programs, which could pre-empt some unforeseen bugs that cause programs to crash."
I hope this is an error on the part of the journalist who wrote the article, because it implies that Turing's halting problem, and Gödel's incompleteness theorems, which lie behind it, are potentially soluble. They aren't. All the more reason for full disclosure.