A mathematically-inclined reviewer (or an LLM) can quickly identify that it's an exploit. (Two exploits; it's crafted to hit a bug in another proof checker, too.)
The post gestures at this, but a natural follow-up, beyond fixing specific bugs around this exploit, would be to task some security-oriented models with proving False in Lean, or with reviewing the code for potentially unsound steps, missing checks, or even useful 'hardening'. That's happening and bugfixes are landing as a result.
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
A mathematically-inclined reviewer (or an LLM) can quickly identify that it's an exploit. (Two exploits; it's crafted to hit a bug in another proof checker, too.)
The post gestures at this, but a natural follow-up, beyond fixing specific bugs around this exploit, would be to task some security-oriented models with proving False in Lean, or with reviewing the code for potentially unsound steps, missing checks, or even useful 'hardening'. That's happening and bugfixes are landing as a result.