If you’re at the state where the worst thing about a proof is that it relies on the axiom of choice, you’re practically at the finish line (at least compared to here). Once proofs has been discovered, mathematicians have a pretty good track record of whittling them down to rest on fewer assumptions. From my (uninformed dilettante’s) perspective, it’s not worth limiting your toolset until you’ve found some solution to your problem. Any solution, even ones which rest on unproven conjectures, will teach you a lot.
What do you mean?
If you’re at the state where the worst thing about a proof is that it relies on the axiom of choice, you’re practically at the finish line (at least compared to here). Once proofs has been discovered, mathematicians have a pretty good track record of whittling them down to rest on fewer assumptions. From my (uninformed dilettante’s) perspective, it’s not worth limiting your toolset until you’ve found some solution to your problem. Any solution, even ones which rest on unproven conjectures, will teach you a lot.
Ah, yes, I think that makes sense. And obviously a proof of say Friendliness in ZFC is a lot better than no proof at all.