The paper proves that Li₂(1/n) = Σr≥1 n−r/r² is irrational for every nonzero integer n. The positive determinant covers 2 ≤ n ≤ 11, the signed determinant covers −7 ≤ n ≤ −2, and a three-form Hermite–Padé construction covers n ≥ 12 or n ≤ −8. Classical evaluations cover n = ±1. The Lean 4 formalization proves the same statement. This page shows its dependency graph, extracted from the compiled Lean environment: every project declaration that the main theorem uses, directly or indirectly, with the axioms each one depends on.
Figure. Dependency graph of the Lean proof.
Three levels. Overview: the parts of the proof. Modules: the Lean files of one part, grouped by folder when there are many. Declarations: one declaration with what it uses and what uses it. Click a node for details; double-click, or use the button in the panel, to open it one level deeper. Arrows point from a user to what it uses. Without a mouse, use the search box and the links in the panel, which reach every node; the parts are also listed in text further down.
Statement
In the paper
For |z| ≤ 1, put Li₂(z) = Σr≥1 zr/r².
Theorem 2.1.For every nonzero integer n, the number Li₂(1/n) is irrational.
The index k starts at 0, so k + 1 runs over r ≥ 1. Irrational is Mathlib's predicate x ∉ range((↑) : ℚ → ℝ).
Axioms
These three are Lean's standard axioms (propositional extensionality, choice, quotient soundness). No sorryAx and no project-specific axiom occurs. The package was built from commit f9768a9c of the development repository (lean/README.md). The independent nanoda checker accepted it on 2026-10-19, before the v2 release (receipt in lean/verification/); the Lean-kernel comparator accepted the same commit on 2026-10-20, after the v2 package freeze. These release checks are separate from this graph build and extraction.
How the parts are formed
The parts follow the paper's coverage map (§2.1) and assembly (§13). The three constructed inputs are the positive determinant (2 ≤ n ≤ 11), signed determinant (−7 ≤ n ≤ −2), and Hermite–Padé tails (n ≥ 12 or n ≤ −8). The direct classical evaluations at n = ±1 belong to the Final argument, with their own anchors. The positive range includes the unconditional base-2 theorem and the common profile for bases 3–11. The Hermite–Padé decay and no-adjacent-zero arguments stay together because they use the same tail representation. The map takes the dependency closure of the concrete producers and generic range consumer for each construction, and separate final anchors for the classical evaluations and range split. Parts are assigned to declarations, not files: exactly one closure gives that part; two or more gives Shared declarations; no closure gives final wiring. A file can hold declarations of several parts and appears in each relevant module view. Certificate data and vendored code are a separate content axis, labelled with the constructions they serve. Generated literal tables and their kernel checks count as data; generic soundness theorems remain proof declarations.
By construction one exclusive construction part cannot use another: whatever it uses lies in its own closure, so it is either its own or shared. That is a consequence of the rule, not a check. The checks below test the extracted graph.
Most-used declarations
Outside certificate data and vendored code, counted by direct uses (uses from certificate data included).