Breakthrough Tracker record
A preprint claims a full proof of Fraenkel’s Beatty-sequence conjecture
Hu Tan and Ying Zhang claim that every exact partition of the integers into at least three Beatty sequences with distinct moduli has Fraenkel’s binary density pattern. Their proof reduces the problem to a dimension-free one-third density theorem, exact finite checks and a deletion induction.
← Back to the filtered Breakthrough Tracker
- Stable ID
math-fraenkel-beatty-sequence-conjecture-proof-2026- Revision
math-fraenkel-beatty-sequence-conjecture-proof-2026.v2- Field
- Mathematics · Number theory, combinatorics and discrete Fourier analysis
- Evidence
- Tier 1 · Peer reviewed: No
- Record state
- Provisional · Provisional claimed proof
- Last checked
AI role
The authors report that GPT-5.6 Sol resolved the cases with 8–11 components and inspired key proof ideas; OpenAI Codex designed, implemented and ran the finite-case verification code; and Ziv supported exploration and checking. They state that the authors determined and verified the mathematics.
Record details
- Problem or result
- Fraenkel’s 1973 classification of exact partitions by distinct Beatty sequences
- Authors
- Hu Tan and Ying Zhang
- Institutions
- Academy of Mathematics and Systems Science, Chinese Academy of Sciences; Soochow University
- Result date
- Preprint v2 submitted October 2, 2026; Lean artifact uploaded the same day
Why it matters
The conjecture links exact integer coverings to a rigid binary pattern and had previously been proved only through seven components. A correct general proof would close the remaining cases uniformly.
Limits
The 38-page v2 remains unrefereed. Its Lean package contains no sorry or admit tokens but declares 13 explicit axioms, including three imported certificate assertions, so it is useful partial formalization evidence rather than an end-to-end derivation from Lean’s foundational axioms.
Sources
- Primary: Tan and Zhang, claimed proof of Fraenkel’s conjecture
- Artifacts: Finite-case verification repository
- Formal artifact: Pinned Fraenkel Lean artifact upload
Correction and revision history
- 2026-09-04 — Added after primary-source, scope, status, AI-role and limitation review.
- 2026-10-05 — Reviewed arXiv v2 and the uploaded Lean package; documented its explicit axiomatic boundary and retained provisional status.
Machine-readable: JSON v1 · CSV v1 · Schema v1
This individual record remains noindex until a story-specific featured image passes Kingy’s rendered-pixel visual review. The source-linked tracker hub remains the public index.