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 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.