Ernst Zermelo exposited the Axiom of Choice in order to prove what is now known as Zermelo's Well-Ordering Theorem.
He himself did not invent the idea of the choice function; he explains that he is merely formalizing a concept ubiquitous in mathematics.
Formulation 1 and formulation 2 are written in a letter from ZermelotoDavid Hilbert, postmarked $24$ September $1904$:
Zermelo wrote formulation 3 in 1908: Neuer Beweis für die Möglichkeit einer Wohlordnung ("A new proof of the possibility of well-ordering") (Math. Ann. Vol. 65: pp. 107 – 128)
Kurt Gödel showed in $1938$ that the Axiom of Choice is not disprovable in Zermelo-Fraenkel set theory (ZF).
Paul Cohen showed in $1963$ that neither is the Axiom of Choice provable in ZF.