I would like to see statements X such that:
(1) We can prove X is true under ZFC.
(2) We do not know whether X can be proven without the axiom of choice.
For example, the statement "every vector space has a basis" does not count, since we know it cannot be proven without the axiom of choice. But if there is a theorem whose proof involves AC, and we do not have a proof that doesn't involve AC, but we don't know that AC is required, that would count.
Here is one of the bigger open problems in choiceless set theory, unfortunately, the concept and proofs are not that immediate.
Theorem. ($\sf ZFC$) Suppose that $\Bbb P$ is a partially ordered set and $G\subseteq\Bbb P$ is a $V$-generic filter, then $V$ is definable in $V[G]$ by a first-order formula using a parameter which lies in $V$.
The proof is relatively straightforward, provided that you have set up all the needed machinery correctly.
We do not know almost anything about this theorem if we only assume $\sf ZF$. The most we know is that if there is a proper class of Löwenheim–Skolem cardinals, then the result holds. But so far, the only scenario we know where this condition holds is when the axiom of choice can be forced with a set forcing.
We can also cheat, and be maximally annoying, and do the following. Let $\varphi,\psi$ be two statements in the language of set theory such that $\varphi$ implies $\psi$ assuming $\sf ZFC$. If the implication is unknown in $\sf ZF$, then $\varphi\to\psi$ is an example.
So, for example, we do know if the Partition Principle implies the Axiom of Choice, that's an example. And we do not know if the uniqueness of an algebraic closure implies its existence. Or if the existence of linear functionals implies the Axiom of Choice, etc.
Now you have a very easy machinery to generate a statement to your liking from pretty much any open problem related to the axiom of choice.
A rather exotic example are the inconsistency theorems by Kunen. The main theorem goes like this: Let $V$ be the class of all sets. Assuming the axiom of choice, there is no proper class $j$ which is a non-trivial elementary embedding $j:V\to V$. An elementary embedding is called trivial, if it is the identity map.
It is not known, whether such embeddings are consistent with $\sf ZF$. I.e. whether there exists a model of $\sf ZF$ (possibly under assumption of some large cardinals) where there is such a non-trivial embedding.
For further reading, consider the Wikipedia "Kunen's inconsistency theorem" or the keyword "Reinhardt cardinal". There you find some references (as of October 2022).
