The paper proves that Li₂(1/2) = Σn≥1 2−n/n² is irrational using determinant polynomials Gm(T), an analytic bound by a logarithmic energy, a common denominator from binomial valuations, and nonvanishing from a Lucas congruence modulo 83. The Lean 4 formalization proves the same statement with no hypotheses. 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.
The index k starts at 0, so k + 1 runs over n ≥ 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 released package also records acceptance by the Lean kernel through the comparator and by the independent nanoda type checker.
How the parts are formed
The paper derives Theorem 1 from three estimates: the analytic bound (1.2), integerization (1.3) and nonvanishing (1.4); §10 combines them. The Lean final theorem li2_half_irrational_of_envelope_v2 has the same shape: it applies an endpoint criterion, which formalizes the §10 argument, to the three estimates. The map takes the dependency closure of the top-level Lean declarations of each estimate and of the endpoint criterion. Parts are assigned to declarations, not files: a declaration reached from exactly one of them belongs to it; a declaration reached from two or more is a shared definition; the few declarations above all of them are the final wiring and belong to the Final argument. A file can hold declarations of several parts; the module view marks such files. Certificate data and vendored code are a separate axis: generated data folders, literal tables with their kernel checks, and third-party sources; each such box is used by exactly one estimate. Generated literal tables and their kernel checks count as data; generic soundness theorems remain proof declarations.
By construction an estimate never uses a declaration of another estimate: 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).