The #1 most popular question on MO is "Examples of common false beliefs in mathematics". - The #8 most popular answer is "[if a set is open, then it is not closed][1]". - The #4 most popular answer is "[1 + the product of the first n prime numbers is always prime][2]". - The #2 most popular answer is "[the trace of a product of any number of matrices is independent of their order][3]" [Here][4] are verifications that these are indeed false beliefs. :) [Alternative link since that one may be down](https://lean.math.hhu.de/#code=import%20Mathlib.Topology.Clopen%0Aimport%20Mathlib.Data.Nat.Prime%0Aimport%20Mathlib.NumberTheory.SmoothNumbers%0Aimport%20Mathlib.Data.Real.Basic%0Aimport%20Mathlib.LinearAlgebra.Matrix.Trace%0Aimport%20Mathlib.Data.Matrix.Reflection%0Aimport%20Mathlib.Tactic.NormNum.Prime%0A%0Aexample%3A%20IsOpen%20(%E2%88%85%20%3A%20Set%20Bool)%20%3A%3D%20trivial%0Aexample%3A%20IsClosed%20(%E2%88%85%20%3A%20Set%20Bool)%20%3A%3D%20isClosed_empty%0A%0Aexample%3A%20%E2%88%83%20n%2C%20%C2%AC%20Nat.Prime%20(((Nat.primesBelow%20n).prod%20(id))%20%2B%201)%20%3A%3D%20by%0A%20%20exact%20Exists.intro%2014%20(Mathlib.Meta.NormNum.not_prime_mul_of_ble%2059%20509%20(59%20*%20509)%20rfl%20rfl%20rfl)%0A%0Adef%20A%E2%82%81%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%20%3A%3D%20!%5B%0A%20%20(!%5B0%2C1%5D)%2C%0A%20%20(!%5B0%2C1%5D)%0A%5D%0Adef%20A%E2%82%82%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%20%3A%3D%20!%5B%0A%20%20(!%5B1%2C1%5D)%2C%0A%20%20(!%5B1%2C0%5D)%0A%5D%0Adef%20A%E2%82%83%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%20%3A%3D%20!%5B%0A%20%20(!%5B1%2C0%5D)%2C%0A%20%20(!%5B1%2C0%5D)%0A%5D%0A%0Ainfix%3A50%20%22%20%C3%97%20%22%20%3D%3E%20(%CE%BB%20A%E2%82%81%20A%E2%82%82%20%E2%86%A6%20Matrix.mul%E1%B5%A3%20A%E2%82%81%20A%E2%82%82)%0A%0Aexample%20%3A%20%E2%88%83%20A%E2%82%81%20A%E2%82%82%20A%E2%82%83%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%2C%0A%20%20%20%20Matrix.trace%20((A%E2%82%81%20%C3%97%20A%E2%82%82)%20%C3%97%20A%E2%82%83)%0A%20%20%E2%89%A0%20Matrix.trace%20((A%E2%82%83%20%C3%97%20A%E2%82%82)%20%C3%97%20A%E2%82%81)%20%3A%3D%20by%0A%20%20exists%20A%E2%82%81%3Bexists%20A%E2%82%82%3Bexists%20A%E2%82%83%0A%0A--%20def%20A%20%3A%3D%20Matrix.mul%E1%B5%A3%20(Matrix.mul%E1%B5%A3%20A%E2%82%81%20A%E2%82%82)%20A%E2%82%83%0A--%20def%20B%20%3A%3D%20Matrix.mul%E1%B5%A3%20(Matrix.mul%E1%B5%A3%20A%E2%82%83%20A%E2%82%82)%20A%E2%82%81%0A--%23eval%20Matrix.trace%20A%20--%201%0A--%23eval%20Matrix.trace%20B%20--%202%0A) [1]: https://mathoverflow.net/a/23580/4600 [2]: https://mathoverflow.net/a/23521/4600 [3]: https://mathoverflow.net/a/23481/4600 [4]: https://live.lean-lang.org/#code=import%20Mathlib.Topology.Clopen%0Aimport%20Mathlib.Data.Nat.Prime%0Aimport%20Mathlib.NumberTheory.SmoothNumbers%0Aimport%20Mathlib.Data.Real.Basic%0Aimport%20Mathlib.LinearAlgebra.Matrix.Trace%0Aimport%20Mathlib.Data.Matrix.Reflection%0Aimport%20Mathlib.Tactic.NormNum.Prime%0A%0Aexample%3A%20IsOpen%20(%E2%88%85%20%3A%20Set%20Bool)%20%3A%3D%20trivial%0Aexample%3A%20IsClosed%20(%E2%88%85%20%3A%20Set%20Bool)%20%3A%3D%20isClosed_empty%0A%0Aexample%3A%20%E2%88%83%20n%2C%20%C2%AC%20Nat.Prime%20(((Nat.primesBelow%20n).prod%20(id))%20%2B%201)%20%3A%3D%20by%0A%20%20exact%20Exists.intro%2014%20(Mathlib.Meta.NormNum.not_prime_mul_of_ble%2059%20509%20(59%20*%20509)%20rfl%20rfl%20rfl)%0A%0Adef%20A%E2%82%81%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%20%3A%3D%20!%5B%0A%20%20(!%5B0%2C1%5D)%2C%0A%20%20(!%5B0%2C1%5D)%0A%5D%0Adef%20A%E2%82%82%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%20%3A%3D%20!%5B%0A%20%20(!%5B1%2C1%5D)%2C%0A%20%20(!%5B1%2C0%5D)%0A%5D%0Adef%20A%E2%82%83%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%20%3A%3D%20!%5B%0A%20%20(!%5B1%2C0%5D)%2C%0A%20%20(!%5B1%2C0%5D)%0A%5D%0A%0Ainfix%3A50%20%22%20%C3%97%20%22%20%3D%3E%20(%CE%BB%20A%E2%82%81%20A%E2%82%82%20%E2%86%A6%20Matrix.mul%E1%B5%A3%20A%E2%82%81%20A%E2%82%82)%0A%0Aexample%20%3A%20%E2%88%83%20A%E2%82%81%20A%E2%82%82%20A%E2%82%83%20%3A%20Fin%202%20%E2%86%92%20Fin%202%20%E2%86%92%20%E2%84%95%2C%0A%20%20%20%20Matrix.trace%20((A%E2%82%81%20%C3%97%20A%E2%82%82)%20%C3%97%20A%E2%82%83)%0A%20%20%E2%89%A0%20Matrix.trace%20((A%E2%82%83%20%C3%97%20A%E2%82%82)%20%C3%97%20A%E2%82%81)%20%3A%3D%20by%0A%20%20exists%20A%E2%82%81%3Bexists%20A%E2%82%82%3Bexists%20A%E2%82%83%0A%0A--%20def%20A%20%3A%3D%20Matrix.mul%E1%B5%A3%20(Matrix.mul%E1%B5%A3%20A%E2%82%81%20A%E2%82%82)%20A%E2%82%83%0A--%20def%20B%20%3A%3D%20Matrix.mul%E1%B5%A3%20(Matrix.mul%E1%B5%A3%20A%E2%82%83%20A%E2%82%82)%20A%E2%82%81%0A--%23eval%20Matrix.trace%20A%20--%201%0A--%23eval%20Matrix.trace%20B%20--%202%0A