qedbot

Erdős·erdos:1196

Erdős Problem 1196

problem formal record: solved source: proved (Lean) F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through a Comparator challenge and an alignment table.

number theory, primitive sets·Source

AI activity

How grades work
GPT-5.4 Pro

13 Apr 2026

Full solution

full A3 V1 F2
Reasoning and sources

Autonomy

AI standalone; human involvement recorded as non-significant

GPT-5.4 Thinking

16 Apr 2026·with Nat Sothanaphan

Full solution (stronger than literature)

full A1 V1 F2
Reasoning and sources

Autonomy

AI collaborating with humans

Gauss

16 Apr 2026·supporting task

GPT-5.4 Pro (2026)

full A1 V1 F2
Reasoning and sources

Autonomy

Secondary contribution: formalization

Details

proof to formalize: GPT-5.4 Pro (2026)

GPT-5.4 Thinking

20 Apr 2026·supporting task

Tao (2026)

full A1 V1 F2
Reasoning and sources

Autonomy

Secondary contribution: rewriting

Details

argument to rewrite: Tao (2026)

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through a Comparator challenge and an alignment table.

reviewed by its authors only

Declared by the projects

1

As each project's formalization.yaml states it.

Erdos1196plby/Erdos1196 · joined by names · no independent check

Read formalization.yaml

authors
Boris Alexeev, Kevin Barreto, Yanyang Li, Jared Duker Lichtman, Liam Price, Jibran Iqbal Shah, Quanyu Tang, Terence Tao
method
agent — ChatGPT, Claude Fable 5
review
self-assessed
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
results
7 main results named, checked with Comparator, with an alignment table
sources
Primitive sets and von Mangoldt chains: Erdos Problem #1196 and beyond — formalizes
checked by
nobody independent of its authors yet

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 1

Recorded elsewhere

Compare the registries
  • vibemathed — Erdős Problem #1196: Primitive Sets

    checked·machine-led·their labels: lean-verified, ai-discovered

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

Cite this record

qed.bot, “Erdős Problem 1196”, https://qed.bot/s/erdos-1196, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.