Some Junk Theorems in Lean

Some Junk Theorems in Lean

This is a small collection of formally verified junk theorems provable in Lean 4 + Mathlib that, in my experience, are quite surprising and upsetting to mathematicians who are not familiar with type theory (and in the case of Theorems 13 and 14, also to mathematicians who are familiar with type theory). See the main .lean file here.

Coding

Theorem 1. The third coordinate of the rational number $\frac{1}{2}$ is a bijection.

Theorem 2. The first coordinate of the polynomial $X^2(X^3 + X + 1)$ is equal to the prime factorization of $30$ .

Theorem 3. Let $P$ be the multivariate polynomial $(X_0 + X_1 + X_2)^3$ . Let $Q$ be the univariate polynomial $X^2 + X + 1$ . The second coordinate of $P$ applied to the first coordinate of $Q$ is equal to the natural number $6$ .

Sets and Logic

Theorem 4. The set $\{z : \mathbb{R} | z

eq 0\}$ is a continuous, non-monotone surjection.

Theorem 5. The Riemann hypothesis is in the topological closure of the set not not.

... continue reading