@tao , "Some of these errors can be mitigated by running different kernels that have been implemented in different programming languages on different hardware and operating systems.". Better than different kernels, different formalization languages. If the bug is in Lean itself, different kernels may reproduce it. But different formalization languages not. Main problem is this is not always possible. "What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI" https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/