For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single use

For the problem to affect proofs, it would have to be in the type checker, and the type system isn’t really that complex. The good news is that every single user of Lean checks this works every day. Finding a flaw that literally everyone relies upon and doesn’t notice is pretty implausible.