Yes, in hindsight it makes sense that a eager LLM would exploit bugs in the kernel itself. I have not read the details yet (but want to!) and assume that it is rather related to the layers directly before or after the type-theory core; i.e. that the AI managed to get a correct typecheck by sidestepping a check during in one of the translation steps somehow, by manipulating the kernels result or by going totally hacker mode and swap implementation/overwrite memory; that is just speculation on my part though, I mainly base if on what I know about Haskell and the https://en.wikipedia.org/wiki/Calculus_of_constructions in general that have not that many constructs, and I would assume the variants used in Rocq and Lean are proven sound.
For experimental features where soundness is not proven, all bets are off IMO, but of course, that does not stop bad actors from engagement knowlingly abusing unsoundness for their own gain. Fortunately, that kind of manipulation is easy to verify when one has access to the codebase; I am would assume that something like lints for experimental features exist, or better even, something like a "sound mode". That does not help against hacking the kernel machinery though.
Concluding notes: - In this particular instance, the Collatz conjecture was appearently chosen on purpose to demonstrate the Kernel bug, from the same thread: "Not that this changes any of the above, but I am informed that the person posting the proof was actually aware that this was a Lean kernel soundness bug, and it was not intended to be taken seriously as a solution to Collatz's problem." - IF the code is made public (and it would be highly suspicious if parts of a proof where hidden), then I would assume this kind of hack is 1) easier to spot that other kinds of hack, since the asset-under-attack is really small and 2) there is not so much incentive to use much time/ingenuity/tokens on finding those hacks (the more are found and fixed, the better of course) 3) and they should be easy to defend against, I would assume; my first thought would be the flag I mentioned above that simply forbids all non-sound features, at the cost of limiting expressive power.
----
Edit: I checked, and I think it alleviates my worries in the sense that the bug(s) where not in the type theory or its implementation, but rather the machinery around it. Further context below:
That is the incident description (also linked in the x thread you linked, for future readers: https://infosec.exchange/@0xabad1dea/117002106099986943).
The following is from that thread or links from it:
- "Fixes two things: (1) more strict/nuanced handling for structure/proj interactions, and (2) adds methods for enforcing that generated auxiliary data for inductives, constructors, and recursors are more strictly checked against the assertions in the export file." | That is the fix to the non-Lean-kernel that was mentioned. To me, (2) looks firmly like what I meant with "supporting machinery", regarding (1), I do not know enough to have an opinion about it (i.e. how on what layer those interactions happen(ed)) | https://github.com/ammkrn/nanoda_lib/pull/22
- "For example, pipeline wedges (execute this instruction and the core freezes and never executes another instruction) would not be found by these techniques..." | Power and limits of Lean | https://infosec.exchange/@david_chisnall/117003914014196496
- "@mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it. There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer." | Computer-checked proofs run on computers, which brings its own attack vectors, independent of how well the kernel is written | https://infosec.exchange/@0xabad1dea/117002712346315184
personal, cautios takeaway after reading the details: If you use Lean4 to write proofs, or read that a reputable group of mathematicians publizised a Lean4 proof, you are still highly unlikely to be fooled by a bug, and if Fable 5 decides to exploit a 0day in the core Lean4 machinery, that should still be able to be caught quickly.