[JacobAsmuth]

You read it yourself :)

If you and the AI agree on the translation of the problem, and lean agrees with the solution, then you're done.