Comment by mrob

There are many independent implementations of Lean's proof checker:

https://arena.lean-lang.org/

It's highly implausible that the same bug is present in all of them.