v0.1.0 — Lean 4 / Mathlib formalization of high-ROI structural lemmas from Zhi-Wei Sun, Catalan's constant is irrational (arXiv:2609.04176v1). Proved: Theorem 2.1, Corollary 2.1 (absolute), det-level Lemma 5.4, Theorem 5.1, Lemma 5.5 ((5.2) and (5.3)), and Corollary 5.2 §5 content. Does not claim Theorem 1.1. Companion numerical note: 10.5281/zenodo.22830610. Source: github.com/chokmah-me/catalan-sun-lean.
Catalan's constant · Lean 4 · Mathlib · formalization · number theory