Can Tarski's circle squaring problem be solved with measurable sets and/or without the Axiom of Choice?

Update: The problem has been solved. See below for the original answer, with the state of the art in 2013.

In 2017, Ł. Grabowski, A. Máthé and O. Pikhurko showed in Measurable circle squaring, Ann. of Math. (2) 185 (2017), no. 2, 671–710, MR3612006, that Tarski's problem can be solved using pieces that are both Lebesgue and Baire measurable. Their proof is almost, but not quite, constructive. Choice is invoked to deal with a small (null, meager) piece.

Their result was then improved to a complete solution of Tarski's problem, where the pieces are not only measurable but in fact Borel sets of low Borel complexity and the decomposition is achieved via a completely explicit procedure, see

MR3702673. Marks, Andrew S.; Unger, Spencer T. Borel circle squaring. Ann. of Math. (2) 186 (2017), no. 2, 581–605.

(The paper is also available at the arXiv.)

The argument builds on Laczkovich's ideas (his discrepancy estimates, which Marks and Unger call the central ingredient in Laczkovich's original result). It also uses flows on Borel graphs and some recent results on hyperfiniteness of free Borel actions.

They state their result as saying that for any $n\ge 1$, any two bounded Borel sets in $\mathbb R^n$ of positive measure and with boundaries of Minkowski dimension strictly less than $n$ are equidecomposable by translations using Borel pieces. (But, as mentioned above, their proof actually gives more, providing an "explicit procedure" for the equidecomposition.)

Original answer: This problem appears to still be open, and not much progress has been made recently (at least, publicly). For the state of the art around 2002, see

Miklós Laczkovich. Paradoxes in measure theory. In Handbook of measure theory, Vol. I, II, E. Pap, ed., pp. 83–123, North-Holland, Amsterdam, 2002. MR1953492 (2003j:28044).

As Miklós explains there and you point out, his proof of equidecomposibility uses the axiom of choice: There is a group being considered, and one uses a set of representative from the cosets. This is akin to forming a Vitali set, though it is not clear that in the present case the resulting sets have to be non-measurable.

In the Handbook article, Miklós mentions two conjectures of Gardner. The first (Conjecture 9.4) states that if two subsets of $\mathbb R^n$ are Lebesgue measurable and equidecomposable under isometries from an amenable group, then they are equidecomposable with measurable pieces. This would imply a positive answer to your question.

The second (Conjecture 9.5) states that if a polytope and a convex body in $\mathbb R^n$ are equidecomposable with Lebesgue measurable pieces under a finite set of isometries from an amenable group, then the pieces in the equidecomposition can be further assumed to be convex.

However, it is impossible to have both conjectures, as it is known that a circle and a square are not equidecomposable using convex pieces. (Gardner has suggested that, all things being equal, perhaps this is evidence that Conjecture 9.5 is false.)

A version of Conjecture 9.4 is true: Suppose $A$ and $B$ are Lebesgue measurable, and equidecomposable under finitely many isometries from an amenable group. Then they are continuously equidecomposable with Lebesgue measurable functions and with the same isometries. Here, if $\chi_H$ is the characteristic function of a set $H$, then we say that $A,B\subseteq\mathbb R^n$ are continuously equidecomposable iff there are functions $f_i:\mathbb R^n\to[0,1]$ and isometries $g_i$, $i=1,\dots,k$, such that $$ \chi_A=\sum_{i=1}^k f_i, $$ and $$ \chi_B= \sum_{i=1}^k f_i\circ g_i. $$ This notion is due to Wehrung, and the result is due independently to Wehrung and Laczkovich.

However, Miklós closes the relevant section of his Handbook article by explaining how this result falls short of a positive answer to Conjecture 9.4.

Let me further add that we really do not know much to be certain one way or the other. It is not even known whether the equidecomposition is impossible using Borel pieces.

Also, almost nothing is known about the required number of pieces in the equidecomposition. Gardner proved that two pieces do not suffice, and that three pieces do not suffice, if the sets are equidecomposable by translations (as in Laczkovich proof). Miklós's argument requires about $10^{40}$ pieces (his original proof used about $10^{50}$).