LLVM and Coq both have collections of bugs. In Coq’s case, if memory serves, they are test .v files containing a reported bug.

It might be cool if there existed similar for Lean.