Criteria and two quadratic instances for Bugeaud's Problem 10.61
Covering criteria for a 1967 equidistribution problem of Mendès France are proved and applied to two quadratic Pisot cases, with Lean checking; the general problem stays open.
- Lab
- Independent
- Model
- Claude Fable 5; Claude Opus 5
- Field
- Mathematics
- Date
- 2026-08-31
- Human collaborators
- Ralf Stephan
- Problem posed
- 1967 · open 59 yrs
Sources
Original work
Independent commentary
What was found
Bugeaud's Problem 10.61, due to Mendès France in 1967, asks whether for a Pisot number alpha and the associated Cantor set of base-alpha expansions with digits 0 and 1, no point of that Cantor set makes the sequence of its multiples by powers of alpha uniformly distributed modulo one. What the repository establishes is narrower than the problem: covering criteria for it, proved only for quadratic setups where alpha is a real root of a quadratic whose conjugate has modulus below one, together with two instances of that kind. Material for arbitrary degree is present but conditional, showing for one family that the large real root is Pisot with a conjugate-modulus bound.
Novelty check
The repository is explicit that the problem remains open and that what is proved are criteria and instances rather than the general statement, so the novelty question is about the criteria rather than the headline. Every compared statement that concludes Problem 10.61 does so in a quadratic setup, and both worked instances are quadratic, because the covering criterion is proved only there; the arbitrary-degree material does not carry any compared statement above degree two. That boundary is recorded in the registry entry as well as in the repository.
Caveats and known objections
Announced through a repository rather than a paper, unrefereed, with no independent check on record. The grade is claimed rather than formal despite a Lean development, because what is machine-checked covers the quadratic criteria and instances rather than the problem, vibemathed records the Lean work as checked with its statement unaudited, and the covering criterion additionally leaves cases open even within the quadratic range. Anyone citing this should treat Problem 10.61 as open. Autonomy is graded ai-led following the registry's record of the models as the source of the results, with the repository owner supplying framing and publication; no author-written AI disclosure has been located.
Machine-checked elsewhere
PalomarPALOMAR-2026-08-31-000013
rwst/Pisot-Cantor-61 at d61132ffcdb7 · checked 2026-09-06
ProvedBB61.QuadSetup.equidistributed_iff_exists_invariant_measureBB61.QuadSetup.forall_not_equidistributed_iff_exists_trigCertificateMeasureTheory.le_integral_of_partitionPressure_leBB61.forall_not_equidistributed_of_partitionPressure_ltBB61.forall_not_equidistributed_of_transferBoundBB61.QuadSetup.routeAExponent_mul_hMinBB61.slope_neg_iffBB61.logb_coverTotal_balancedDepth_leBB61.QuadSetup.exists_avoided_intervalBB61.QuadSetup.not_equidistributed_of_routeAExponent_lt_oneBB61.QuadSetup.routeAExponent_lt_one_iff_quadraticBB61.isPisot_familyBB61.norm_le_familyConjBoundBB61.routeA_family_lt_oneBB61.routeA_two_add_sqrt5BB61.two_add_sqrt5_not_equidistributedBB61.GapThree.problem_10_61_two_add_sqrt3_axiom_free
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
What typechecks is the criteria and the two quadratic instances, not Problem 10.61. BB61.QuadSetup.routeAExponent_lt_one_iff_quadratic is where that boundary is visible: the covering criterion is characterized only for quadratic setups, and the arbitrary-degree material carries no compared statement to the problem. Every compared statement depends on propext, Classical.choice and Quot.sound and nothing else. Palomar also carries the submitter's own disclosure that he has not verified informal-to-formal fidelity, and that the challenge file governs wherever the prose disagrees with it.
Also recorded at
vibemathedbugeaud-problem-10-61
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
History of this entry
- CheckedPalomar registered the Lean development as PALOMAR-2026-08-31-000013, mechanically confirming that it typechecks against seventeen stated theorems at a pinned commit. The grade stays at claimed: what is checked is the quadratic criteria and instances, and Problem 10.61 remains open.
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Criteria and two quadratic instances for Bugeaud's Problem 10.61. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-31-pisot-cantor-equidistributionBibTeX
@misc{whataifound-independent-2026-equidistribution,
title = {Criteria and two quadratic instances for Bugeaud's Problem 10.61},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-08-31-pisot-cantor-equidistribution}
}