OEIS A049473 in Lean 4

This repository targets the single research open theorem OeisA49473.conjecture at Formal Conjectures commit e13dd7284e72012a1616806d09cb6b8025e387af.

Although the theorem is one declaration, its proposition is a conjunction of two claims:

1. a pair of inequalities for the tail of the series for ζ(3);
2. a classification of the zero and one positions in the difference sequence of A049473.

Both conjuncts are required to solve the Formal Conjectures target.

Open Lean4Web and load or paste lean4web/OeisA49473Lean4Web.lean. The standalone file imports only mathlib and reproduces the Formal Conjectures definitions locally.

At the pinned commit, the exact target is:

@[category research open, AMS 11]
theorem OeisA49473.conjecture :
    (∀ n : ℕ, 1 ≤ n →
      s (a n) < 1 / (n : ℝ) ^ 2 ∧
      1 / (n : ℝ) ^ 2 < s (a n - 1)) ∧
    (∀ n : ℕ, 1 ≤ n →
      let diff : ℕ := a n - a (n - 1)
      (diff = 0 ↔ n - 1 ∈ A001954) ∧
      (diff = 1 ↔ n - 1 ∈ A001953)) := by
  sorry

The file in lean/ imports those exact definitions. It does not use the upstream OeisA49473.conjecture, because the proof of that declaration currently contains sorry. Instead, both versions prove tail_target and beatty_target independently and combine them in oeis_a049473_conjecture_solved, whose displayed type is the raw conjunction above.

Write

a(n) = ⌊n / √2 + 1/2⌋,
R_m  = ζ(3) - ∑_{k=1}^m 1/k³.

For m ≥ 1, two termwise telescoping comparisons give

R_m     < 1 / (2m(m + 1)),
R_{m-1} > 1 / (2m² - 2m + 1).

With m = a(n), the nearest-integer condition implies the integer bounds

2m² - 2m + 1 ≤ n² ≤ 2m(m + 1).

Taking reciprocals and combining the inequalities proves

R_m < 1/n² < R_{m-1}.

The step a(n) - a(n - 1) is always zero or one. Direct floor inequalities show that the positions of the one steps are

⌊(k + 1/2)√2⌋,                    k ≥ 0,

which is A001953. The zero steps occur at

⌊(k + 1/2)(2 + √2)⌋,            k ≥ 0,

which is A001954. The complementary factor identity

(2 + √2)(1 - 1/√2) = 1

relates the two floor conditions; irrationality of √2 excludes endpoint equality.

Each directory contains one Lean source file, lakefile.toml, lean-toolchain, and a generated lake-manifest.json.

Formal Conjectures version:

cd lean
lake update
lake exe cache get
lake build
lake env lean -DwarningAsError=true OeisA49473FC.lean

Standalone mathlib/Lean4Web version:

cd lean4web
lake update
lake exe cache get
lake build
lake env lean -DwarningAsError=true OeisA49473Lean4Web.lean

The public proof files contain no sorry, admit, custom axiom, native_decide, or unsafe declaration. Their final #print axioms commands record the axioms used by the proved results. Both package builds succeed on Lean 4.27.0; the combined theorem uses only propext, Classical.choice, and Quot.sound.

What is kernel-checked here:

Both conjuncts, combined in one theorem with the exact Formal Conjectures proposition.

What this repository does not change by itself:

The public status of Formal Conjectures or OEIS.

At the pinned snapshot, Formal Conjectures still marks the declaration research open, and the OEIS entry still labels the 2014 statement as a conjecture. Changing those public records requires a reviewed upstream contribution.

• OEIS A049473
• OEIS A001953
• OEIS A001954
• Formal Conjectures: OEIS/49473.lean
• Repository layout used as a model

This formalization was developed with assistance from OpenAI Codex.