Here is a nice example.

Theorem. Space $\newcommand\R{\mathbb{R}}\R^3$ is the disjoint union of circles.

The AC proof is simply to enumerate all points in $\R^3$ in a well-ordered sequence in length continuum, and then attach a circle to each point along the way. If at stage $\alpha$ the $\alpha$th point is not yet occuring on a circle, then since we have chosen already only fewer than continuum many circles, there must be a plane through the point that is not coplanar with any of them. And since each circle already chosen intersects that plane in at most two points, there are fewer than continuum many forbidden points on the plane. And so we can find a circle through that point in that plane that avoids them.

Meanwhile, there is a constructive proof given as theorem 1.1 of

• M. Jonsson and J. Wästlund: Partition of R3 into curves, Mathematica Scandinavica 83 (1998) 192-204; JSTOR, author's website.

One places circles of radius 1 centered at (4k+1,0,0), and then considers spheres centered at the origin, which intersects that family always in exactly 2 points, and such a 2-punctured sphere can be partitioned by circles. (Note: the proof is constructive in the sense that it does not use AC, but it is not constructive in the sense of intuitionistic logic.)

Of course it is nice to have the specific construction, but to my way of thinking, the AC proof is far more flexible, and one can use to to construct many other kinds of partitions (into unit circles, shapes of other kinds etc etc), whereas specific constructions for many of these other instances remain as open questions.

Here is another similar instance:

Theorem. Space can be partitioned by skew lines.

The AC proof proceeds like the transfinite recursion above. Just add the next point, using a line pointing in a totally different direction to the previous lines.

But there is a constructive proof also. Take one vertical line, and then a nested arrangement of hyperboloids, with gradually changing angles. Each of them is a union of straight lines, and these are all skew.

See these related MO questions:

• Covering space by disjoint unit circles
• Is it possible to partition $\R^3$ by disjoint unit circles?
• Foliating space by skew lines
• Concerning proofs from the axiom of choice that ℝ³ admits surprising geometrical decompositions: Can we prove there is no Borel decomposition?

The latter question can be seen as asking which of these AC arguments genuinely require something fundamentally nonconstructive.

Here is a nice example.

Theorem. Space $\newcommand\R{\mathbb{R}}\R^3$ is the disjoint union of circles.

The AC proof is simply to enumerate all points in $\R^3$ in a well-ordered sequence in length continuum, and then attach a circle to each point along the way. If at stage $\alpha$ the $\alpha$th point is not yet occuring on a circle, then since we have chosen already only fewer than continuum many circles, there must be a plane through the point that is not coplanar with any of them. And since each circle already chosen intersects that plane in at most two points, there are fewer than continuum many forbidden points on the plane. And so we can find a circle through that point in that plane that avoids them.

Meanwhile, there is a constructive proof given as theorem 1.1 of

• M. Jonsson and J. Wästlund: Partition of R3 into curves, Mathematica Scandinavica 83 (1998) 192-204; JSTOR, author's website.

One places circles of radius 1 centered at (4k+1,0,0), and then considers spheres centered at the origin, which intersects that family always in exactly 2 points, and such a 2-punctured sphere can be partitioned by circles. (Note: the proof is constructive in the sense that it does not use AC, but it is not constructive in the sense of intuitionistic logic.)

Of course it is nice to have the specific construction, but to my way of thinking, the AC proof is far more flexible, and one can use to to construct many other kinds of partitions (into unit circles, shapes of other kinds etc etc), whereas specific constructions for many of these other instances remain as open questions.

Here is another similar instance:

Theorem. Space can be partitioned by skew lines.

The AC proof proceeds like the transfinite recursion above. Just add the next point on a line avoiding the previous lines and pointing in a totally different direction.

But there is a constructive proof also. Take one vertical line, and then a nested arrangement of hyperboloids, with gradually changing angles. Each of them is a union of straight lines, and these are all skew.

See these related MO questions:

• Covering space by disjoint unit circles
• Is it possible to partition $\R^3$ by disjoint unit circles?
• Foliating space by skew lines
• Concerning proofs from the axiom of choice that ℝ³ admits surprising geometrical decompositions: Can we prove there is no Borel decomposition?

The latter question can be seen as asking which of these AC arguments genuinely require something fundamentally nonconstructive.

Here is a nice example.

Theorem. Space $\newcommand\R{\mathbb{R}}\R^3$ is the disjoint union of circles.

The AC proof is simply to enumerate all points in $\R^3$ in a well-ordered sequence in length continuum, and then attach a circle to each point along the way. If at stage $\alpha$ the $\alpha$th point is not yet occuring on a circle, then since we have chosen already only fewer than continuum many circles, there must be a plane through the point that is not coplanar with any of them. And since each circle already chosen intersects that plane in at most two points, there are fewer than continuum many forbidden points on the plane. And so we can find a circle through that point in that plane that avoids them.

Meanwhile, there is a constructive proof given as theorem 1.1 of

• M. Jonsson and J. Wästlund: Partition of R3 into curves, Mathematica Scandinavica 83 (1998) 192-204; JSTOR, author's website.

One places circles of radius 1 centered at (4k+1,0,0), and then considers spheres centered at the origin, which intersects that family always in exactly 2 points, and such a 2-punctured sphere can be partitioned by circles.

Of course it is nice to have the specific construction, but to my way of thinking, the AC proof is far more flexible, and one can use to to construct many other kinds of partitions (into unit circles, shapes of other kinds etc etc), whereas specific constructions for many of these other instances remain as open questions.

Here is a nice example.

Theorem. Space $\newcommand\R{\mathbb{R}}\R^3$ is the disjoint union of circles.

The AC proof is simply to enumerate all points in $\R^3$ in a well-ordered sequence in length continuum, and then attach a circle to each point along the way. If at stage $\alpha$ the $\alpha$th point is not yet occuring on a circle, then since we have chosen already only fewer than continuum many circles, there must be a plane through the point that is not coplanar with any of them. And since each circle already chosen intersects that plane in at most two points, there are fewer than continuum many forbidden points on the plane. And so we can find a circle through that point in that plane that avoids them.

Meanwhile, there is a constructive proof given as theorem 1.1 of

• M. Jonsson and J. Wästlund: Partition of R3 into curves, Mathematica Scandinavica 83 (1998) 192-204; JSTOR, author's website.

One places circles of radius 1 centered at (4k+1,0,0), and then considers spheres centered at the origin, which intersects that family always in exactly 2 points, and such a 2-punctured sphere can be partitioned by circles. (Note: the proof is constructive in the sense that it does not use AC, but it is not constructive in the sense of intuitionistic logic.)

Of course it is nice to have the specific construction, but to my way of thinking, the AC proof is far more flexible, and one can use to to construct many other kinds of partitions (into unit circles, shapes of other kinds etc etc), whereas specific constructions for many of these other instances remain as open questions.

Here is another similar instance:

Theorem. Space can be partitioned by skew lines.

The AC proof proceeds like the transfinite recursion above. Just add the next point, using a line pointing in a totally different direction to the previous lines.

But there is a constructive proof also. Take one vertical line, and then a nested arrangement of hyperboloids, with gradually changing angles. Each of them is a union of straight lines, and these are all skew.

See these related MO questions:

• Covering space by disjoint unit circles
• Is it possible to partition $\R^3$ by disjoint unit circles?
• Foliating space by skew lines
• Concerning proofs from the axiom of choice that ℝ³ admits surprising geometrical decompositions: Can we prove there is no Borel decomposition?

The latter question can be seen as asking which of these AC arguments genuinely require something fundamentally nonconstructive.