[math-fun] 73 digit factor found with ECM