Erdős problem 394 · problems.science

For the least $t_k(n)$ with $n \mid t_k(n)(t_k(n)+1)\cdots(t_k(n)+k-1)$ , do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with $c = 1/2048$ admissible in the $t_2$ bound.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/394.lean

Formal Conjectures

FormalConjectures/ErdosProblems/394.leanErdos394.erdos_394.parts.i1 lineExact file

1True ↔ ∃ c > 0, (fun x => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑(Erdos394.t 2 n)) =O[Filter.atTop] fun x => ↑x ^ 2 / Real.log ↑x ^ c

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

William Blair Lean proofswilliamjblair:Research.erdos394_first_question_proved
William Blair Lean proofswilliamjblair:Research.erdos394_second_target_proved

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

argument
VibeMathed
Machine
GPT-5.6 starships (Claude Fable 5 reviewer)
Reported outcome
candidate
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science