AI Proof WatchKeep up with AI contributions

AI-led Lean proof gives a quadratic orbit-gap criterion

For a quadratic real root α>1 of X²−aX−b whose conjugate has modulus below one, the Route A exponent condition A(α)<1 gives an open interval missed by every orbit (ξαⁿ mod 1) with ξ in the paper’s class C(α), so none is uniformly distributed. The criterion is equivalent to (log₂α−1)(log₂(α/|b|)−1)>1 and yields an explicit gap for α=2+√5.

Sources for this record

What was already known

Mendès France’s non-equidistribution question appears as Bugeaud Problem 10.61. The full problem remains open, and the source does not establish historical priority for this quadratic criterion.

AI involvement AI-led

Stephan set the targets and directed the project. The source credits Claude Opus 5 agents with the mathematics and Lean proofs; Stephan says he cannot independently reconstruct the informal argument.

The source assigns the mathematical development of the quadratic criterion and instance to the agents, while Stephan chose targets and directed the work.

Importance Modest

Gives a formalized sufficient condition and a specific quadratic instance of orbit non-equidistribution.

Limitations

It does not cover all Pisot numbers above 2 or any degree above two. The separate α=2+√3 gap is outside this criterion.

Technical verification Formal (Lean 4/Mathlib kernel and Comparator)

The cited source reports that Comparator matched the 17 named declarations against the flat challenge, checked their permitted axioms and replayed the exported proofs through the Lean kernel. The rating covers the Route A quadratic criterion and α = 2 + √5 declarations, not the unbridged higher-degree ingredients, tables or all of Problem 10.61. This review did not rerun Lean.

Formal checking

statement and definition comparison, permitted-axiom audit and exported-proof kernel replay

Checker
Repository Comparator and Lean kernel
Scope
The named std3-flat declarations, including BB61.QuadSetup.not_equidistributed_of_routeAExponent_lt_one, routeAExponent_lt_one_iff_quadratic, exists_avoided_interval and BB61.two_add_sqrt5_not_equidistributed
Basis
Reported by the linked checker
Evidence source

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

Human understanding Few

Stephan explicitly disclaims the ability to reconstruct the arguments. The available explanatory notes were agent-written, and no later human account of the central mechanism was found.

Correction and publication history

2026-10-18 · publication

Gives a formalized sufficient condition and a specific quadratic instance of orbit non-equidistribution.

Read this published revision