qedbot

Erdős·erdos:1045

Erdős 1045

problem formal record: unclassified source: open 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 an alignment table and written divergences.

analysis·Source

AI activity

How grades work

No AI contribution recorded against this statement.

Claimed on erdosproblems.com

1

Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through an alignment table and written divergences.

declares divergences from its source reviewed by its authors only

Declared by the projects

1

As each project's formalization.yaml states it.

Eventual maximizers of the planar distance productRogerhu12/Erdos1045 · joined by names · no independent check

Read formalization.yaml

authors
Boyang Hu
method
agent — GPT-5.6 Luna, GPT-5.6 Sol, GPT-6 Astra
review
self-assessed
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
sources
Eventual maximizers of the planar distance product — formalizes; Erdős problem 1045 — background
related
coleski/erdos1045-n6/tree/59ede5a12403d62d00fa21b59597dbb6c01fb0a2 — independent
divergences
Global analytic localization uses an exterior-map/Faber route in place of the manuscript's capacity-based localization argument. Activity of constraints is proved using feasible lens-coordinate variations before KKT. Finite-kernel monotonicity uses exact difference identities and function-value convergence. The diameter graph is expressed by the explicit cyclic adjacency predicate CanonicalEvenDiameterAdj. The algebraic certificate specifies the reference construction, polynomial system and window explicitly, and proves existence and uniqueness of the selected root. The explicit even-order extension uses quantitative Fourier, localization, pressure and Schur estimates to prove the displayed integer cutoff. Explicit localization and uniform local rigidity give the smaller common threshold for odd diameter and perimeter maximizers. The quantitative pressure margin, radial derivative and chart estimates also establish unique strictly positive KKT multipliers at the same even-order cutoff.
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 · 0

No formal statement located.

Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 1
  • https://www.erdosproblems.com/1045

Cite this record

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

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