Comment by bmacho

The single most best definition I know is what is on the wiki[0]:

> A choice function (also called selector or selection) is a function f, defined on a collection X of nonempty sets, such that for every set A in X, f(A) is an element of A. With this concept, the axiom can be stated:

> Axiom—For any set X of nonempty sets, there exists a choice function f that is defined on X and maps each set of X to an element of that set.

I like this definition because IMO it is simple, close to the name of the axiom, and you might want to use it in this form, that is, having a set of sets, and taking a choice function on them.

To understand its importance and the controversies around it, you'll need some examples and counterexamples how truthness and provability and knowability (regarding structures, numbers, metamathematics) interact; also what are the views of the majority of working mathematicians and people in other fields using mathematics.

[0] : https://en.wikipedia.org/wiki/Axiom_of_choice#Statement

Tangential, but a choice function is one of the ur-examples of Dependent Type Theory (DTT). In standard ZFC the choice function on X would have the type signature

   f: X -> UX (union X).

And you know the additional information that (∀A:X) (f(A) ∈ A), which is not encoded in the type signature, just an additional fact that you know, and have to keep track of it. In DTT the codomain can be the function of the picked element of the domain. In this case, the DTT type signature of f would be

   f: (A:X) -> A.

So in this case the signature of the function carries strictly more information than in the case of normal, static function type signatures in ZFC. And the axiom of choice simply states that the type (A:X) -> A is non-empty if every A are non-empty.