I'm not in the field, but afaik most of the work is done with the Lean proof assistant[1] which uses logic that is already formally verified to be true. The LLMs typically bridge the gap between the original problem statement and a proper Lean definition that then can be processed by the Lean software.
I think there are more details, but this is the gist of it. However, you need to manually verify that the LLMs produce Lean definitions that actually match your problem statement.
They're using Rocq