[dehsge]

LLMs and its output are bounded by Rices theorem. This is not going to ensure correctness it’s just going to validate that the model can produce an undecidable result.

[ogogmad]

Errr, checking correctness of proofs is decidable.