there is a proof in lean4 it's correct by construction

How do you know that what is being proved in the lean code is the same as the millennium prize criteria though?

you can get another LLM to verify / if the lean doesn't have `sorry` used to skip certain parts of the proof etc. It's much easier once it's in lean4 because checks like that can be done computationally.