I'm a dumb guy, so please excuse me in advance, but how do you verify the verification code is doing what it says its doing (verifying). If the answer is "another verifier" - how many turtles do you need to make this work?
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.
loading story #50213898