Papers With

← All papers
First page of Higher derivatives of the Gram function

Higher derivatives of the Gram function

Marius Dundulis, Ramūnas Garunkštis, Antanas Laurinčikas, Raivydas Šimėnas

math.NT Oct 12, 2026 · v1
formalization number-theory analysis ai-agents
Read PDF arXiv abstract Code
TL;DR
Formalizes asymptotics of higher derivatives of S(t) and Gram functions and uniform distribution results in Lean 4, with code written largely by LLMs.
Abstract
We study the nonlinear phenomenon of the asymptotics of higher-order derivatives of the Gram function $t_u$. We also prove the uniform distribution and continuous uniform distribution modulo one of $t^n_u$ for $n = 1, 2, \dots$. We use AI to formalize our proofs in Lean.
Problem

The work studies the asymptotics of higher-order derivatives of the Gram function t_u and of the related functions S(t) and the Riemann-Siegel theta function. It also asks whether the powers t_u^n are uniformly distributed modulo one, in both the discrete and continuous sense.

Approach

Asymptotic formulas for S^{(n)}(t) are derived from the Riemann-von Mangoldt formula, using differentiation under the integral sign for the error term δ(t). Uniform distribution follows from a monotonicity criterion on derivatives. The results were formalized in Lean v4.29.1, with code written using Claude Opus and other LLMs. In the formalization, S is generalized to a class of functions built from arbitrary step functions with discrete jump sets.

Results

The paper proves S^{(n)}(t) = (-1)^{n-1}(n-2)!/(2π) t^{1-n} + O(t^{-n-1}) and the uniform distribution modulo one of t_u^n. The Lean project has over 10,000 lines, builds without sorry, uses only standard axioms, and is publicly available on GitHub.