However, LLMs aren't capable of writing proofs. They can only regurgitate text that looks like a proof by training on proofs already written. There's no reasoning behind what they produce. So why waste the time of a human to review it?
If the provers' kernel and automation make the proof pass but it makes no sense, what use is it?
People write proofs to make arguments to one another.
However, LLMs aren't capable of writing proofs. They can only regurgitate text that looks like a proof by training on proofs already written. There's no reasoning behind what they produce. So why waste the time of a human to review it?
If the provers' kernel and automation make the proof pass but it makes no sense, what use is it?
People write proofs to make arguments to one another.