When asking whether or not an axiom can be proven, we need to ask "relative to what?" In other words, what axioms would we be allowed to use to prove it. Usually the answer here is something along the lines of "all of the other axioms".
Here, we typically take the 'other axioms' to be the ZF axioms of set theory. It is known that the axiom of choice is not a logical consequence of the ZF axioms. This was proven by Paul Cohen in the 1960s. What he showed, essentially, is that if there is a structure that satisfies the ZF axioms, then there is a structure that satisfies the ZF axioms but not AC. It had been shown earlier by Godel that if there is a structure that satisfies the ZF axioms, then there is one that satisfies ZF and the axiom of choice (ZFC). So the axiom of choice is truly independent of the other axioms.
It is useful to compare this to the situation with Euclid's parallel postulate, as I see people already doing in the comments. People thought for a long time that it must be provable from the other axioms. Let's call the other axioms neutral geometry NG. Of course a long time later, the mystery was solved why you could not prove the parallel postulate. There are structures that satisfy the NG axioms and also satisfy the parellel postulate (Euclidean geometry) and structures that satisfy the NG axioms but don't satisfy the parallel postulate (non-Euclidean geometries). It simply turned out that the other axioms were not sufficient to fully pin down Euclidean geometry, because there are multiple types of geometry that differ on whether the parallel postulate is true (and how it fails if it does).
Similarly, assuming ZF is consistent, there are many different universes of sets that are models of ZF, and they differ from one another on whether the axiom of choice is true.
Another useful comparision that's often made is to group theory. The axioms of group theory say that there are elements and a binary operation between them that obey certain properties. We find many structures that obey the axioms of group theory... we call them groups. There are many statements that are independent of the axioms of group theory. For instance $$\forall (x,y)\; x\cdot y = y\cdot x$$ is independent of the axioms of group theory since there are both abelian and non-abelian groups.
Similarly the axioms of ZF are that there are some elements (called sets) and a binary relation between them $\in$ such that $x\in y$ is interpreted as "$x$ is an element of $y$." We call a structure that obeys ZF a "model of ZF" (doesn't have a snappy name like "group"). Cohen and Godel showed that the axiom choice is independent of the ZF axioms just like the "commutativity axiom" is independent of the axioms of group theory.