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.