Erdős problem 796 · problems.science

If $g_3(n)$ is the largest size of $A \subseteq [1,n]$ with fewer than three representations of every product $a_1 a_2$ , does its conjectured second-order normalized term converge? The candidate proof gives an explicit limit constant.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/796.lean

Formal Conjectures

FormalConjectures/ErdosProblems/796.leanErdos796.erdos_7961 lineExact file

1True ↔ ∃ c, Filter.Tendsto Erdos796.normalizedError Filter.atTop (nhds 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:Erdos796.erdos796_statement

Reported activity

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

Valid but non-improving proofs
GPT-Erdős
Open the source record
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