qedbot

Erdős·erdos:346

Erdős Problem 346

problem formal record: solved source: solvedno F1 unaudited

Machine-checked by qed.bot.

Fidelity F1: A formal artifact exists, but nothing records that its statement says what the claim says.

number theory, complete sequences·Source

AI activity

How grades work
Codex, GPT-5.5 Pro

2026-06-19

Solution to variant problem (Lean)

partial A3 autonomous V3 checked F1 unaudited
Reasoning and sources

Autonomy

AI standalone, with comparable literature existing

Details

literature: 🟡 Burr and Erdős (1981)

literature found on: 20 Jun, 2026

similar?: Yes

Codex, GPT

2026-06-21·with Kenta Kitamura

Full solution (Lean)

full A1 collaborative V3 checked F1 unaudited
Reasoning and sources

Autonomy

AI collaborating with humans

Does the formal statement say what was claimed?

F1 unaudited A formal artifact exists, but nothing records that its statement says what the claim says.

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

Checks

1
  • verified qed.bot

    346 theorems on the standard axioms only

    proof rebuilt and axioms inspected·2026-08-22

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Formal material

Formal statements · 1
Cited proofs · 0

No proof artifact cited by the formal record.

Recorded elsewhere

Compare the registries
  • vibemathed — Erdős Problem #346

    checked·joint·their labels: lean-verified, ai-co-developed

Also known as · 3
  • https://www.erdosproblems.com/346
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/346.lean
  • FormalConjectures/ErdosProblems/346.lean