The hugging face attack shows that you don’t need to direct AI at finding a bug in the Lean kernel. Translating the hugging face attack to this scenario: You just need to give it a math problem it believes is more difficult then finding a lean kernel exploit. And since it is now public knowledge that lean has had kernel soundness bugs in the past, any pretrained model might see this as a possibility of passing their task.
The hugging face attack shows that you don’t need to direct AI at finding a bug in the Lean kernel. Translating the hugging face attack to this scenario: You just need to give it a math problem it believes is more difficult then finding a lean kernel exploit. And since it is now public knowledge that lean has had kernel soundness bugs in the past, any pretrained model might see this as a possibility of passing their task.