Motivation This question came from my efforts to solve this problem presented by Andre Weil in 1951.
Can we prove the following theorem without Axiom of Choice?
Theorem Let $A$ be an integrally closed domain containing a field $k$ as a subring. Suppose $A/fA$ is a finite $k$-module for every non-zero element $f \in A$. Then the following assertions hold.
(1) Every ideal of $A$ is finitely generated.
(2) Every non-zero ideal of $A$ is invertible.
(3) Every non-zero ideal of $A$ has a unique factorization as a product of prime ideals.
EDIT May I ask the reason for the downvotes? Is this the reason for the downvotes?
EDIT What's wrong with trying to prove it without using AC? When you are looking for a computer algorithm for solving a mathematical problem, such a proof may provide a hint. At least, you can be sure that there is a constructive proof.