AI Proof WatchKeep up with AI contributions

AI agents extend a difference-free construction to all powers

For every k≥2, a nonempty pool of ranked blocks on pairwise coprime square-free moduli, with ranks strictly decreasing along nonzero k-th-power-residue difference arcs, gives α(k,P)≤liminf log D_k(N)/log N and eventually D_k(N)≥N^ρ for every ρ<α(k,P). Two separate nine-block instances give α(4,P₄)=0.912145042700…>0.9121 and α(6,P₆)=0.950825559086…>0.9508; each exceeds the specified six-residue Ruzsa-transfer comparator.

Sources for this record

What was already known

Krachun used ranked blocks for square differences (k=2), obtaining exponent 0.7527964558…. Ruzsa’s digit transfer already applied to general k. The specified comparator exponents are 0.908103… for k=4 and 0.949759… for k=6.

AI involvement AI-led

JD Jones set the objective. Claude Fable and Claude Opus agents developed the general-k theorem, Lean proof and search that found the k=4 and k=6 block pools. Jones maintained the project but reports no independent human mathematical review.

The source attributes the general-k proof architecture and the retained searched blocks to Claude agents, with Jones directing the target.

Importance Notable

The construction extends the directed method to every k≥2 and improves the two specified lower-bound comparators.

Limitations

The comparators are not established as the global best previous bounds, and optimality of the new block pools is not claimed.

Technical verification Formal (Lean 4/Mathlib kernel with exact finite `decide` checks and a project axiom audit)

The repository reports complete Lean 4 proofs of the ten selected statements, ordinary kernel `decide` checks of the blocks and numeric inequalities, a source guard, an axiom audit and statement comparison. A separate Python block check corroborates the finite data; this review did not rerun the checks.

Formal checking

compiled formal proofs, kernel evaluation of eighteen blocks and thirty-eight power comparisons, source guard and standard-axiom audit

Checker
Lean 4 kernel and project axiom audit
Scope
KthPower.directed_liminf, directed_pointwise, pool4_valid, pool6_valid, the exponent comparisons and their two liminf instances
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

The proof explanation is agent-written and no named human explanation or independent human mathematical review of the general-k construction is documented; Few is an evidence-gap default, not a finding that Jones cannot understand it.

Correction and publication history

2026-10-18 · publication

The construction extends the directed method to every k≥2 and improves the two specified lower-bound comparators.

Read this published revision