Sir Deenicus said:
He did not go out and "discover" consequences from axioms but instead experimented with mathematical concepts to get what it is he wanted.
At one point, Fermat did not know that a certain formula was true, and later found through proof that it was true. Perhaps people don't go out and discover consequences, but they consider propositions that interest them, and discover
that said propositions are consequences. Mathematicians don't discover sentences, they discover
that sentences are theorems, and in that sense (what other sense do you think we meant) theorems are discovered.
Discovery figures little into it. Here again we see a clash of concepts that do not transfer well.Given a powerful enough computer it is not too far fetched that all that follows from a set of axioms can be generated in a very small time. Or even, at once.
I can't see how this is relevant. Personally, I would argue that if we found that we could program a computer to generate all the theorems, and then printed them out and discovered a sentence p on that list, then we've discovered that p is a theorem. However, even if finding out that p is a theorem in this way doesn't count as discovery, the point remains that mathematicians do nothing of this sort. If I think that I can prove p to be a theorem, and work at it and found out that p does in fact follow as a theorem, then I've discovered
that it is a theorem. The suggestion that perhaps a person reading a print out of all the theorems of Peano arithmetic cannot be said to discover any theorems doesn't affect, whatsoever, that I still might have.
Suppose one person discovers for himself that a box B contains an object O. Suppose a second person is simply told that B contains O. Will you argue that the first person did not discover that B contains O because the second person was told it? What does one even have to do with the other?
Ofcourse not, he had a character in mind and drew from his experiences to assign it basic properties that he felt it should have based on his needs. I no longer see where the original point of contention lies although i suspect it has to do with our definitons of the word invent.
Hamlet is Danish because it pleased Shakespeare that he be a Dane. Fermat's proposition is not a theorem simply because it pleased Fermat that said proposition be a theorem. It was entirely Shakespeare's invention that Hamlet be a Dane. It wasn't Fermat's invention that his proposition be a theorem. He had a proposition, and found out that it was a theorem. (Actually, I'm unsure of the history, and whether he actually proved it. I think I remember reading/hearing that he had scribbled it in the margin of some paper, but I think Euler might be credited with its proof).
Again, Fermat did not work from axioms. I do not see why you state your opions as fact. There are those who believe mathematics to have a creative aspect, and thus requiring imagination and creativity in one's creations. Certainly it can be done mechanically but that is but a small aspect of the whole endeavour. I believe it has already been concluded that no one computer can ever replace mathematicians.
Sure, mathematics does have a creative aspect. In particular, it requires creativity to
find out that p is a theorem. It also requires creativity to
decide that Hamlet will be a Dane. The fact that creativity is used in both is irrelevant. What's relevant is that in the first case, the "theoremness" of a statement is found out, or discovered. In the second case, Hamlet's nationality was decided, made up, invented.
Again, I don't think that everything in mathematics can be said to be invented, nor do I think everything in mathematics is invented. Perhaps some things are discovered, some things are invented, some are both, and some are neither. Mathematics has many things: a formal language, definitions, theorems, problems, propositions, methods, etc. However, on the specific point of whether a given formula is a theorem, it is discovered that it is a theorem, and it is not invented that it is a theorem.