Junk Theorems in Lean

4 months ago

A collection of formally verified junk theorems in Lean 4 + Mathlib that surprise mathematicians unfamiliar with type theory.
Theorem 1: The third coordinate of the rational number 1/2 is a bijection.
Theorem 2: The first coordinate of the polynomial X²(X³ + X + 1) equals the prime factorization of 30.
Theorem 3: The second coordinate of a multivariate polynomial applied to the first coordinate of a univariate polynomial equals 6.
Theorem 4: The set {z : ℝ | z ≠ 0} is a continuous, non-monotone surjection.
Theorem 5: The Riemann hypothesis is in the topological closure of the set not not.
Theorem 6: The binary expansion of 7 is equivalent to itself.
Theorem 7: The dot product of not with itself and the matrix determinant of or, but not of and.
Theorem 8: The existential quantifier on the category of groups is a non-measurable set.
Theorem 9: ζ(1) = ½(γ - log 4π), where ζ(s) is the Riemann zeta function.
Theorem 10: 2 - 3 (as a partial function on ℕ) equals +∞.
Theorem 11: The unique proofs of quadratic reciprocity and the Baire category theorem not being false are equal in pointed types.
Theorem 12: Complex relationships between coordinates of polynomials and rational numbers.
Theorem 13: a = b = c, showcasing issues with definitional proof irrelevance in Lean.
Theorem 14: Assuming certain axioms, 0 = 1, highlighting inconsistencies in Lean's compiler design.

Hasty Briefsbeta