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.
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.
[1] https://en.wikipedia.org/wiki/Lean_(proof_assistant)