Bugs found in the kernel as a result of formalizationSeptember 23, 2025 ยท View on GitHub https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Soundness.20bug.3A.20hasLooseBVars.20is.20not.20conservative/near/521286338 https://github.com/leanprover/lean4/issues/10475 https://github.com/leanprover/lean4/issues/10511