It’s specifically modern LLMs that might soon make this more practical than clear writing. But this capability isn’t working well enough yet, and this paper seems to be about doing things manually, which won’t necessarily work out better for this group than clear writing did. The formal statements of some theorems and the definitions these theorems (but not the proofs) rely on still need to clearly express the interesting/relevant claims. So there is room for obscurity (by formulating such theorems in strange ways or with dependencies on non-standard definitions) until it’s feasible for others to independently formalize these things, as a problem statement and a challenge for a group that claims to have answers (that somehow persist in remaining inscrutable).
If they provide a working lean proof, it will be so much easier to review the work.
Still, it’s an important point to make. There is still the unverifiable bridge from statement of a theorem in lean to the interpretation of what that statement means. I’ve used LLMs to attempt to formalize pdfs, and a big challenge is making sure all of the assumptions listed before the statement of the main theorem mean what I think they mean.
It’s specifically modern LLMs that might soon make this more practical than clear writing. But this capability isn’t working well enough yet, and this paper seems to be about doing things manually, which won’t necessarily work out better for this group than clear writing did. The formal statements of some theorems and the definitions these theorems (but not the proofs) rely on still need to clearly express the interesting/relevant claims. So there is room for obscurity (by formulating such theorems in strange ways or with dependencies on non-standard definitions) until it’s feasible for others to independently formalize these things, as a problem statement and a challenge for a group that claims to have answers (that somehow persist in remaining inscrutable).
If they provide a working lean proof, it will be so much easier to review the work.
Still, it’s an important point to make. There is still the unverifiable bridge from statement of a theorem in lean to the interpretation of what that statement means. I’ve used LLMs to attempt to formalize pdfs, and a big challenge is making sure all of the assumptions listed before the statement of the main theorem mean what I think they mean.