I would like to point out that a lot of the people who are interested in the Axiom of Choice (AC) are not worried about it in any mathematical way.

In general, I think "Why do people worry about X?" is primarily psychological. I can (and alas, do) worry about the correctness of my proofs for lots of reasons...but fundamentally I am worried about myself and not about some mathematical object or principle.

In fact, I don't see what there is to worry about concerning AC. We know it is independent of ZF, we know it has some counter-intuitive consequences, and we know that many of our most basic and fundamental "abstract" theorems either require AC to hold in full generality (in the sense that there are models of ZF in which they are false) or in fact are equivalent to AC: e.g. every vector space has a basis (equivalent), the product of quasi-compact spaces is quasi-compact (equivalent), every field has an algebraic closure (required), every ring has a maximal ideal (equivalent),...I think we have all the information that we need on the role of AC in mathematics.

On the other hand, if you encounter a theorem, it is often an interesting question to ask whether the proof uses AC and, if it does, whether it can be modified so as not to require AC or only to require some weaker form of AC. As an example, I asked the following MO question

How much choice is needed to show that formally real fields can be ordered?

and the answer was a reference to a paper where it was shown that the orderability of formally real fields is equivalent to the Boolean Prime Ideal Theorem. This is an interesting paper; I learned more about field theory (not set theory) by reading it.

Why is it interesting to ask whether a proof requires AC? For starters, for good reasons (not worries!) people are interested in making proofs constructive as much as possible. You say that you've proven that for every number field $K$, and positive integer $n$, there exists a genus one curve $C_{/K}$ such that the least degree of a closed point on $C$ is equal to $n$? (Yes, I have.) OK, I'll give you $K$ and $n$: can you give me an explicit set of defining equations defining such a curve? (No, I can't!) My theorem would be better if it could be made explicit -- it's obvious, isn't it?

It is a generally believed "meta-theorem" that if a result can be shown to require AC, then it is certifiably non-constructive. Thus, if one is trying to make a certain result constructive, one would certainly like to know whether AC is essentially involved in its proof.

I would like to point out that a lot of the people who are interested in the Axiom of Choice (AC) are not worried about it in any mathematical way.

In general, I think "Why do people worry about X?" is primarily psychological. I can (and alas, do) worry about the correctness of my proofs for lots of reasons...but fundamentally I am worried about myself and not about some mathematical object or principle.

In fact, I don't see what there is to worry about concerning AC. We know it is independent of ZF, we know it has some counter-intuitive consequences, and we know that many of our most basic and fundamental "abstract" theorems either require AC to hold in full generality (in the sense that there are models of ZF in which they are false) or in fact are equivalent to AC: e.g. every vector space has a basis (equivalent), the product of quasi-compact spaces is quasi-compact (equivalent), every field has an algebraic closure (required), every ring has a maximal ideal (equivalent),...I think we have all the information that we need on the role of AC in mathematics.

On the other hand, if you encounter a theorem, it is often an interesting question to ask whether the proof uses AC and, if it does, whether it can be modified so as not to require AC or only to require some weaker form of AC. As an example, I asked the following MO question

How much choice is needed to show that formally real fields can be ordered?

and the answer was a reference to a paper where it was shown that the orderability of formally real fields is equivalent to the Boolean Prime Ideal Theorem. This is an interesting paper; I learned more about field theory (not set theory) by reading it.

Why is it interesting to ask whether a proof requires AC? For starters, for good reasons (not worries!) people are interested in making proofs constructive as much as possible. You say that you've proven that for every number field $K$, and positive integer $n$, there exists a genus one curve $C_{/K}$ such that the least degree of a closed point on $C$ is equal to $n$? (Yes, I have.) OK, I'll give you $K$ and $n$: can you give me an explicit set of defining equations defining such a curve? (No, I can't!) My theorem would be better if it could be made explicit -- it's obvious, isn't it?

It is a generally believed "meta-theorem" that if a result can be shown to require AC, then it is certifiably non-constructive. Thus, if one is trying to make a certain result constructive, one would certainly like to know whether AC is essentially involved in its proof.

I would like to point out that a lot of the people who are interested in the Axiom of Choice (AC) are not worried about it in any mathematical way.

In general, I think "Why do people worry about X?" is primarily psychological. I can (and, alas do) worry about the correctness of my proofs for lots of reasons...but fundamentally I am worried about myself and not about some mathematical object or principle.

In fact, I don't see what there is to worry about concerning AC. We know it is independent of ZF, we know it has some counter-intuitive consequences, and we know that many of our most basic and fundamental "abstract" theorems either require AC to hold in full generality (in the sense that there are models of ZF in which they are false) or in fact are equivalent to AC: e.g. every vector space has a basis (equivalent), the product of quasi-compact spaces is quasi-compact (equivalent), every field has an algebraic closure (required), every ring has a maximal ideal (equivalent),...I think we have all the information that we need on the role of AC in mathematics.

On the other hand, if you encounter a theorem, it is often an interesting question to ask whether the proof uses AC and, if it does, whether it can be modified so as not to require AC or only to require some weaker form of AC. As an example, I asked the following MO question

How much choice is needed to show that formally real fields can be ordered?

and the answer was a reference to a paper where it was shown that the orderability of formally real fields is equivalent to the Boolean Prime Ideal Theorem. This is an interesting paper; I learned more about field theory (not set theory) by reading it.

Why is it interesting to ask whether a proof requires AC? For starters, for good reasons (not worries!) people are interested in making proofs constructive as much as possible. You say that you've proven that for every number field $K$, and positive integer $n$, there exists a genus one curve $C_{/K}$ such that the least degree of a closed point on $C$ is equal to $n$? (Yes, I have.) OK, I'll give you $K$ and $n$: can you give me an explicit set of defining equations defining such a curve? (No, I can't!) My theorem would be better if it could be made explicit -- it's obvious, isn't it?

It is a generally believed "meta-theorem" that if a result can be shown to require AC, then it is certifiably non-constructive. Thus, if one is trying to make a certain result constructive, one would certainly like to know whether AC is essentially involved in its proof.

I would like to point out that a lot of the people who are interested in the Axiom of Choice (AC) are not worried about it in any mathematical way.

In general, I think "Why do people worry about X?" is primarily psychological. I can (and alas, do) worry about the correctness of my proofs for lots of reasons...but fundamentally I am worried about myself and not about some mathematical object or principle.

In fact, I don't see what there is to worry about concerning AC. We know it is independent of ZF, we know it has some counter-intuitive consequences, and we know that many of our most basic and fundamental "abstract" theorems either require AC to hold in full generality (in the sense that there are models of ZF in which they are false) or in fact are equivalent to AC: e.g. every vector space has a basis (equivalent), the product of quasi-compact spaces is quasi-compact (equivalent), every field has an algebraic closure (required), every ring has a maximal ideal (equivalent),...I think we have all the information that we need on the role of AC in mathematics.

On the other hand, if you encounter a theorem, it is often an interesting question to ask whether the proof uses AC and, if it does, whether it can be modified so as not to require AC or only to require some weaker form of AC. As an example, I asked the following MO question

How much choice is needed to show that formally real fields can be ordered?

and the answer was a reference to a paper where it was shown that the orderability of formally real fields is equivalent to the Boolean Prime Ideal Theorem. This is an interesting paper; I learned more about field theory (not set theory) by reading it.

Why is it interesting to ask whether a proof requires AC? For starters, for good reasons (not worries!) people are interested in making proofs constructive as much as possible. You say that you've proven that for every number field $K$, and positive integer $n$, there exists a genus one curve $C_{/K}$ such that the least degree of a closed point on $C$ is equal to $n$? (Yes, I have.) OK, I'll give you $K$ and $n$: can you give me an explicit set of defining equations defining such a curve? (No, I can't!) My theorem would be better if it could be made explicit -- it's obvious, isn't it?

It is a generally believed "meta-theorem" that if a result can be shown to require AC, then it is certifiably non-constructive. Thus, if one is trying to make a certain result constructive, one would certainly like to know whether AC is essentially involved in its proof.