Given a set of axioms and proofs it's possible to mechanically check a proof. It's not quite possible to reliably check proofs otherwise.
Realizing that axioms were switches to be turned on and off to generate new structures that may or may not be useful was an important step to abandoning the most obvious and intuitive truths of geometry. Thus geometry has no concept of true outside of axioms, and true simply means internally coherent. Outside of formalization, "obviously true" is the hindrance of confidence.
You do, if you want to be right. The fact that you can get people to agree with you doesn't make you right, and red is frequently darker than black by some pretty normal definitions of "darker". Red and black are differentiated by the shape of their reflective spectrum, not the amplitude.
pavelrub's point is that you sometimes have less reason to believe the axioms of your formalization than their derived consequences. We have better reason to believe the intuitive idea that 2+2=4 than we do any putative axioms of arithmetic. If we derived that 2+2=5 from some particular axioms of arithmetic, we would conclude those axioms were wrong (or rather, were not the proper system for formalizing 2-plus-2-ness) rather than conclude that 2+2=5.
If you want to argue about what #600000 and #FF0000 should look like, you're back to a rigorous theory of color.
But the whole argument about colors is really unnecessary, I only used it because I thought it would be simpler to understand, but I might have been wrong. If you don’t think that it supports my argument about 2+2=4, feel free to ignore it and address the argument itself.
So you're using a numeric representation of colors (RGB) to prove to me that black is darker than red.
By doing this, you're basically proving my point.
1) different people may have different opinions on "obvious" statements
2) the simpler the statement is, the easier it is to accept or reject it
If you give me two color plates, one is black, and one is red, I might find people who disagree which one is darker.
But if you give me photo measurements, I will say that one is objectively darker with respect to a specific metric (e.g. visible photon energy flux, YCbCr luminosity, CIECAM02 luminosity).
No, I’m not doing that at all - I’m simply creating a well-defined understanding between us about which colors we are talking about, so that there won’t be any confusion. If you were sitting next to me, I could show you some other two colors in person, with no reference to RGB or to any other numeric representation, and the exact same argument would stand.
No specific metric can ever show that #FF0000, as it is displayed on any reasonably well-balanced monitor, is darker than #600000. If somebody invented such a metric, we would say that this metric is either incorrect, or misuses the word “darker”. This would also be the case if no other metrics existed before it. Therefore it is clear that our understanding that #FF0000 is darker than #600000 is independent of any formal description of darkness, and comes prior to it.
And you are still avoiding, for some reason, my main argument, which had nothing to do with colors, and dealt specifically with 2+2=4.
To some extent, there is the problem. People trust their intuitions, and their intuitions are often wrong. That's why for some things we need proper proofs.
Personally I'm more likely to believe 2 + 2 = 4, something I can easily check to my own satisfaction using four objects, than I am to believe the Axiom of Choice.
As for the axioms in use, I think the big reasons they were chosen is: They lead to results we already wanted/proved to be true.
Another thing to keep in mind, not everyone works with the same sets of axioms. Which, as someone with a formalist view on mathematics, I find interesting. For example, not everyone studying logic assumes the principle of the excluded middle. One of the consequences of this is that you can no longer do proofs by contradiction.
The axiom of choice is another example of this where two groups of mathematicians accept it or not. I'm a formalist, so I don't have issues with this (as long as both sets of axioms are interesting and "intuitive"), other philosophies of maths might.
The caveat is that this is non-trivial and it's very easy to make people accept assumptions which are completely wrong. That's really the main reason to accept the axioms of set theory: People have been trying to poke holes in them for a hundred years and nobody has managed it yet. If you can use set theory (or something equiconsistent) to solve your problem, chances are that nobody will be able to call you out on a mistake.