They actually used Lean statements that were carefully human-written and human-reviewed, from here 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.