finding record / formal-conjectures
recordedvf_2df66520d12cbb35
vf_2df66520d12cbb35
Canonical assertion
The Lean 4 theorem `Erdos257.erdos_257.variants.tsum_top_eq` is proven and kernel-verified (axioms: propext, Classical.choice, Quot.sound; no sorryAx): the Lambert-series identity ∑_{n≥1} 1/(2^n - 1) = ∑_{n≥1} d(n)/2^n, where d(n) is the number of divisors of n. Closes a previously-open, UNCLAIMED `sorry` (category: textbook) in google-deepmind/formal-conjectures Erdős Problem 257.
Notation is rendered from the stored source. The pinned checkout remains the exact record.
- model_output
- theoretical
- 1 spans
- recorded
Scope and conditions
theoretical
domain:analytic_number_theory; verifier:lean4_kernel; category:textbook; result:lambert_series_divisor_identity; open_sorry_closed:true; unclaimed_upstream:true
Provenance summary
- cap_beef856ac1c8e4ce · vc_d4db833b655a5bda
- model_output
- Jun 14, 2026, 12:00 AM
- not recorded
- 1
Exact record identityFinding ID, frontier identity, and pinned Git source
- vf_2df66520d12cbb35
- vfr_97d7d25957384f80
- 2705e4db4ffb9987c53388c8a89c1450c63afdf8
- a24f2c67b52a5b3c9163438243b95351bbc8e296
Exact source and rootsGit 2705e4db4ffb and content-addressed ledgers
Source identity
- Commit
- 2705e4db4ffb9987c53388c8a89c1450c63afdf8
- Tree
- a24f2c67b52a5b3c9163438243b95351bbc8e296
- Committed
- 2026-07-19T05:13:20Z
- Repository
- Open source
Content roots
- Event log
- sha256:c4a00883ab7468dcce59c368b81fd09e45366b21af8e34979d7a639d73a8d32c
- Snapshot
- sha256:45fa712bd6d9a8d4c8514a7cba107e7f814f2c1368805abd577e762ccb6123a4
- Proposals
- sha256:ba47ddf5c16ed567ddf835385066e3fc294b447bc0eabd3f9820f5e707efb39e
- Actor registry
- sha256:f52d59b1db885f467c66a29335ada68544a09da5f3869723461100eed0aac79e
- Artifacts
- sha256:fbd7e05b185cd06bc06484e8b0216c17c5263a71d8481ca38e574e9b2c5156d8