Some Junk Theorems in Lean

Summary

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. Note though that showing that the Riemann hypothesis is in the topological closure of not will win you a million dollars. Theorem 6. The following are equivalent: The binary expansion of $7$ . Theorem 7. The dot product of not with itself. Moreover, the matrix determinant of or. However, not the determinant of and. Theorem 8. The existential quantifier on the category of groups is a non-measurable set. Partiality Famously, Lean, like many proof assistants, defines division so that $\frac{1}{0} = 0$ and subtraction on the natural numbers so that $2 - 3 = 0$ . In the first case, this leads to the following theorem (which is already in Mathlib). Theorem 9. ( riemannZeta_one ) $\zeta(1) = \frac{1}{2}(\gamma - \log 4 \pi)$ , where $\zeta(s)$ is the Riemann zeta function. If we try to avoid the junk theorem $2 - 3 = 0$ with the partial subtraction function psub , we get the following. Theorem 10. Two minus three, where subtraction is understood to be a partial function on $\mathbb{N}$ , is equal to t...