Really awesome post. Just some questions below because the 2% you gave is rather low and my personal estimate would easily be off by an order of magnitude (closer to 20%). So the questions below are meant to see where that difference is coming from.
"I am 2% certain that we will soon be putting huge amounts of trust into Lean4 certificates produced by misaligned AIs."
Can I ask you more precisely where your 2% is coming from? I.e. can you give some separate odds for the two closely related statements?
1) We will soon be putting huge amounts of trust into Lean... (read more)
Is there a way of finding a list of guarded definitions on which the lesswrong community has settled on a meaning? I know https://www.lesswrong.com/w/pivotal-act is labeled as such. It would be helpful for me if this page would contain a short description how to find guarded definitions on this website.
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.