# AI provenance: The number of terms in greedy Fibonacci–Lucas representations

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X)
and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914).

- Paper: https://github.com/creelie/musical-rotary-phone/blob/main/preprintKimberlingConjecture/KimberlingConjecture.pdf
- Lean formalisation and code: doi:10.5281/zenodo.23385265 (release v2.0.0; all versions doi:10.5281/zenodo.23315122)
- Repository: https://github.com/creelie/musical-rotary-phone

## Result

Let a(n) be the number of terms in the greedy representation of n by the
Fibonacci and Lucas numbers (OEIS A214973), W(n) = a(1) + ... + a(n), and V(n)
the number of Zeckendorf summands of 1, ..., n. The paper proves three
conjectures stated in the OEIS:

- **Kimberling** (A214981; J. Integer Seq. 23 (2020), Article 20.9.5): V(n)/W(n)
  has a limit in (1.2, 1.4). The limit is (5 − √5)/2, and
  |W(n) − (1/5) n log_φ n| ≤ 10n, |V(n) − (c/5) n log_φ n| ≤ 10n for every n ≥ 1.
- **Greathouse** (A214973): a((F_{3j+1} − 1)/2) = j, and this is the first
  occurrence of j.
- **Kurkov** (A214973): a(n) = A329320(A048679(n)) for n > 0.

## Who did what

Deep Bhattacharjee chose the problem, directed the work, set the format and
the target journal, and ran the computations. Claude (Anthropic), used through
Claude Code under his direction, produced the following:

- the proofs;
- the Lean 4 formalisation;
- the checking programs in C, C++, Python, Julia and shell;
- the figures;
- the LaTeX text of the paper.

No other AI system took part. The paper uses no unproved result from other
work.

## How the result is checked

- **Lean 4.34.1 with Mathlib.** Ten theorems cover every statement of
  Theorems 1.4 to 1.6 of the paper: the bounds on T and Z, the two formulas
  with log_φ n, the limit (5 − √5)/2, Kimberling's conjecture, Greathouse's
  conjecture with the first-occurrence statement, and Kurkov's formula. The
  sequences are defined from their OEIS definitions. Each theorem depends only
  on the standard axioms propext, Classical.choice and Quot.sound. There is no
  `sorry`, `admit`, `native_decide` or added axiom.
- **Independent programs.** Programs in C, C++, Python, Julia and shell
  compute the sequences directly and check the identities and bounds on long
  initial ranges.
- **Release workflow.** It builds the Lean proof and runs every program before
  publishing.

## What is not claimed

The paper proves the three conjectures above and nothing more. The authors
checked on 15 October 2026 that the OEIS entries A214981 and A214973 still
state them as conjectures, and found no other proof on arXiv or the web.