The core of a proof checker is a formally validated core that is based on a small amount of concepts. Every single line in the proof reduces to that core, therefore, as long as you can trust the core, you can trust the execution of the proofs.
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.