# Irrationality of Catalan’s constant

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Catalan's constant is irrational](../../preprints/Catalans-constant-is-irrational-September-24-2026/paper.pdf)

## Scope

The formalization proves that Catalan's constant $G=\sum_{j=0}^{\infty}(-1)^j/(2j+1)^2$ is irrational. This is the mathematical assertion in the paper's title.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Irrationality of Catalan's constant | [Catalan.lean](../ComparatorChallenges/Catalan.lean) |