Also makes me wonder if it found and exploited (or got caught out by) some bugs in the Lean programming language…

(Not saying Lean is buggy, but finding bugs seems more likely to me, as a programmer who knows not much about mathematical proofs since I haven’t looked at anything like that since uni, about a decade ago)