|
|
|
|
|
|
by twotwotwo
3 hours ago
|
|
|
This thread has some context. A proof-system researcher found some proof-system bugs and presented them a funny way: 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. |
|
|