[EE84M3i]

> there is no doubt that the proof is correct.

Do you have any links to reading about how often lean core has soundness bugs or mathlib has correctness bugs?