Is there any chance these will uncover bugs in Lean?
Reading the account from Scott's wife, the proofs seem to resemble more a Zelda speedrun with a bunch of strangely exploited bugs than an actual thing.
A bug in the soundess of Lean would allow for much more ambitious statements to be made, by the Principle of Explosion, so I think it's unlikely. A subtle bug in how something is defined is possible (I don't know the extent to which the community has checked/guarded against this), although I suspect an issue would show up reasonably quickly when one tried to apply one of the results.
Reading the account from Scott's wife, the proofs seem to resemble more a Zelda speedrun with a bunch of strangely exploited bugs than an actual thing.