Mechanical proofs of the Levi commutator problem