The line between axiom and theorem Consider the intermediate value theorem. The theorem is very intuitive and may be described as obvious: if you go from $A$ to $B$ without teleporting, you have been everywhere between $A$ and $B$. However, this theorem is introduced in Calculus. In my case, I saw the theorem at my first uni-level math course. My question is: why is this regarded as a theorem requiring formal proof? When do we simply accept something as an obvious fact? (Even though the latter is something that generally should be avoided in mathematics.) 
 A: The simplest example is the following:
Assume that we are living in a "rational world", and consider the function
$$f:\quad{\mathbb Q}\to{\mathbb Q},\qquad x\mapsto f(x):=x^2\ .$$
Then $f(0)=0$ and $f(2)=4$, but there is no $\xi\in{\mathbb Q}$ with $f(\xi)=2$.
So the "obvious fact" is not so obvious at all. It has something to do with the extra numbers present in ${\mathbb R}\setminus{\mathbb Q}$. Therefore the question arises, how many "extra numbers" do we have to fill in to guarantee the existence of a $\xi$ with $f(\xi)=2$, and a the same time the existence of solutions to myriads of other equations we could come up with. The "completeness axiom" answers this question once and for all; but a lot of work has to be done to show that the enlarged system ${\mathbb R}$ still has the algebraic properties (encoded in the "field axioms") we are so familiar with.
A: The intermediate-value theorem can be taken as an axiom for the algebraic abstraction of $\,\Bbb R\,$ known as a real-closed field R. Below are some of many known equivalent axiomatizations:


*

*There is an ordering on R making it an ordered field such that, in this ordering, the intermediate value theorem holds for all polynomials over R.

*There is a total order on R making it an ordered field such that, in this ordering, every positive element of R has a square root in R and any polynomial of odd degree with coefficients in R has at least one root in R.

*R is not algebraically closed but its algebraic closure is a finite extension.

*R is not algebraically closed but its extension field $\,\rm R(\sqrt{-1})$ is algebraically closed.
A: When something can be proven, given what our already-accepted as axioms, along with definitions, and  already-proven theorems, then prove it, first and foremost. If you don't know whether it can be proven, try to prove it, and if you can't, try to find a counterexample.
An axiom might be postulated when we are paving new way into uncharted territory which is not addressed by current axioms or theories, and only sparingly. But it should merely be postulated, meaning one needs to stipulate that the "axiom" in question is being assumed to be true. 
(But caution! Imagine how embarrassing it would be to "assume" what clearly seems obvious, only to have someone else come along with a contradiction that results from its assumption!)
A: If we were only studying "smooth" curves (whatever that may mean), then there would be argument for not bothering to prove the Intermediate Value Theorem. However, the continuous functions, as defined using the formal "$\epsilon$-$\delta$" definition of continuity, can be much weirder than the smooth curves of our imagination.
For instance, there are continuous functions that are nowhere differentiable. Moreover, such functions can be useful, for instance in modeling Brownian motion!
A: There is a way of using mathematics where one treats a large number of intuitively obvious statements as true facts that can be used whenever you want. For practical matters like architecture, surveying, accounting, measuring, ... this is fine and seldom gets you into trouble.
However, over the years, as people have started paying attention to mathematics for its own sake, we have realized that some of these intuitively obvious statements are in fact false! (For example, they might contradict other parts of mathematics that we find even more obvious.) These unexpected revelations caused people to examine the foundations of mathematics more carefully.
Currently, our standard of rigorous mathematics is as follows: we define a very small number of axioms that capture what we believe to be true about sets, arithmetic, the real numbers, and so on. From these we must prove any other facts we believe to be true. Mathematicians have decided that this structure best allows us to distinguish between intuitively obvious but false statements and intuitively obvious and true statements - and, along the way, has enabled us to discover some extremely counterintuitive yet still true statements. (Not to mention that different people's intuition can disagree in the first place!)
One example of all this is the existence of irrational numbers. It seems to have been regarded as intuitively obvious to the ancient Greeks that all numbers were rational. The discovery of the irrationality of $\sqrt2$ came as quite a shock to them. Its irrationality made very little difference to practical uses of mathematics: you can still measure out a rope whose length is as close to $\sqrt2$ as you care to make it. But it did change our understanding of mathematics for its own sake.
Regarding the intermediate value theorem specifically, note that it fails for functions whose domain is the rational numbers rather than the real numbers (e.g., $x^2-2$). So its truth must depend on some property of the real numbers that the rational numbers don't possess. Understanding these differences has contributed to our description of the foundations of mathematics.
Edited to add: I came across this paper by Stephen M. Walk which expounds upon some of these ideas (intuition in mathematics, for example) but proposes a different justification for the proof of the intermediate value theorem: rather than helping to verify that our intuition about continuous functions is rigorously correct, he says the IVT helps to verify that our rigorous $\epsilon$-$\delta$ definition of continuity accurately captures our intuition!
A: There is a historical reason why the intermediate value theorem is regarded as an important theorem, rather than an axiom.
At one stage the intermediate value property was treated as if it characterised continuous functions - so it might be assumed to be an axiom of continuity.
But then there emerged various problematic functions like $f(x)= \sin \frac 1x$ close to $x=0$, where the value of $f(x)$ at $x=0$ - which has to be defined - can be chosen from the closed interval $[-1,1]$ - and whatever choice is made the the function has the intermediate value property.
Since then even more extreme functions, like the Conway Base 13 function have been discovered. This function has the intermediate value property on any interval - in fact it takes all real values somewhere on any interval - and is nowhere continuous.
So a new definition of continuity was required - but to be a definition of continuity, it had to have all the expected properties. So the intermediate value property had to be proved from the new definition to show that the definition made proper sense.
A: It should be regarded as a theorem requiring proof since it needs results that imply it.  For instance, the Intermediate Value Theorem requires completeness of the real numbers, or that every bounded set has a supremum.  Since this is a weaker result used to prove a stronger result, we demand that the stronger result require proof. 
A: You could just take it as an axiom, by adding it to the usual axioms:
Definition. A real number system is a Dedekind-complete totally ordered field satisfying the intermediate value property.
However, this means the following. Suppose we have a $\mathbb{R}$-like entity, call it $X,$ and we wish to prove that $X$ is in fact a real number system. Then not only do we need to prove that $X$ is a Dedekind-complete totally ordered field, but we also need to prove that $X$ has the intermediate-value property! This is clearly inefficient. Better to prove that the usual axioms imply the intermediate-value property, and be done with it.
On the other hand, it would be perfectly reasonable to axiomatize $\mathbb{R}$ via a completely different approach to the usual (namely, the approach of a Dedekind-complete ordered field). In this case, one of your axioms could easily be the intermediate-value property. You'd probably want to make sure your axioms were independent, though, to avoid the aforementioned inefficiency issue.
