# AI-use and process summary

*Low-discrepancy quasi-uniform digital sequences in every dimension*, version 1 — Leonhard Gruenschloss. Supplementary disclosure (ancillary file; it is not part of the paper).

## Statement

The constructions, proofs and Lean formalization were produced by an AI system (Anthropic Claude Opus 5.5) under the author's direction. The author selected the problems, steered the research and reviewed the formal statements, but has not verified every proof by hand; the computer-assisted parts are exact finite computations whose scope is stated with each result. AI systems are not listed as authors; responsibility for this work rests with the author.

## Systems used

- **Anthropic Claude**, run as agentic sessions in Claude Code: one coordinating session per working day, which
  delegated work to sub-agents (parallel sessions of the same model with their own tools: shell, compilers,
  Python, Lean). Model version: Claude Opus 5.5 (`claude-opus-5-5`), for all of the work (constructions, proofs,
  manuscript, Lean formalization, deposit preparation).
- **Tools run by the agents:** C++ (g++) and Python (uv; numpy, sympy) for searches, exact certificates and
  independent re-implementations; Lean 4 (`v4.35.0-rc3`) with Mathlib; Comparator with the Lean kernel and NanoDa.

## What the AI systems did

- Explored constructions (finite searches over check vectors and window systems, small-case enumeration), proposed
  conjectures and proved them; wrote every proof in the manuscript.
- Wrote the C++/Python programs and the exact certificates of the computer-assisted parts, including independent
  second implementations by separate agents (the archive of the paper, `archive/` of https://github.com/lgruen/quasi-uniform-sequences-lean).
- Drafted the manuscript and its revisions, and ran adversarial review rounds: separate agents tried to refute
  statements, recomputed the printed numbers, checked label references and statement-versus-proof consistency, checked
  the literature credits, and acted as referees of whole revisions.
- Drafted the Lean statements from the manuscript, developed the Lean proofs (the library GeoSeq, which extends the
  Lean library of the companion nets paper; 59 configurations with 730 compared theorems for the results new in
  this version, and a separate Palomar entry), and ran Comparator.
- Built the interactive explainers (https://lgruen.github.io/quasi-uniform-sequences-lean/explainers/), whose computations are cross-checked against the paper's
  numbers.

## What the author did

- Chose the problems and the research direction (quasi-uniform digital sequences, the questions of Dick, Goda and
  Suzuki and of Goda, Hofer and Suzuki; the decision to aim for explicit constructions; scope decisions).
- Steered the work: redirected unproductive routes, required that negative results be stated as evidence rather than
  as impossibility unless proved, required independent verification of claims before they entered the paper, and
  approved compute spending.
- Selected the results that form the paper, and reviewed the formal statements: the four statements of the Palomar
  entry and its public abstract were reviewed against the manuscript and signed off on 2026-10-29. The statements of
  the other library theorems the author accepts on the basis of statement-review notes prepared in AI-assisted review
  passes (each formal statement related to the printed statement by its label, with every divergence); recorded
  2026-10-29.
- Has read parts of the manuscript but has not verified every proof by hand; human understanding is therefore declared
  as "some".

## Time span

This line of work ran from 2026-10-17 to 2026-10-29 (the first version of the manuscript and its Lean formalization),
following the nets paper (hexagon:2610.00217v1).

## Verification layers

1. Lean 4 + Mathlib: the formalized results (listed in the paper's appendix on the Lean development) are accepted by
   Comparator with the Lean kernel and NanoDa; two headline results are a separate Palomar entry (PALOMAR-2026-10-29-000041).
2. Every computer-assisted item is checked by at least two programs, the second written from the statements of the
   paper only; the data with their verifiers are archived (https://github.com/lgruen/quasi-uniform-sequences-lean, directory `archive/`; Zenodo doi:10.5281/zenodo.23769767).
3. Partial human reading by the author.

## Links

- Repository (Lean formalization, LaTeX source, archive): https://github.com/lgruen/quasi-uniform-sequences-lean (release v1.0.0 = version 1)
- Zenodo archive: https://doi.org/10.5281/zenodo.23769767 (concept DOI, all versions); release v1.0.0: https://doi.org/10.5281/zenodo.23769768
- Interactive explainers: https://lgruen.github.io/quasi-uniform-sequences-lean/explainers/
- Palomar entry: PALOMAR-2026-10-29-000041 (https://palomar-registry.org/entry?id=PALOMAR-2026-10-29-000041&version=1)
- Companion paper: *Low-discrepancy quasi-uniform digital nets in every dimension*, hexagon:2610.00217v1 (https://hexagonmath.org/abs/2610.00217v1)