A machine-checked solution to the Jacobians challenge