They actually used Lean statements that were carefully human-written and human-reviewed, from here https://github.com/google-deepmind/formal-conjectures/blob/ma

They actually used Lean statements that were carefully human-written and human-reviewed, from here https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millenium/NavierStokes.lean https://github.com/google-deepmind/formal-conjectures/blob/m... This doesn't guarantee that the statement is correct (Lean cannot do that), but makes it highly likely.