Corroborate

Claim in Erdős problems that formal-conjectures marks solved

A published paper or arXiv preprint answers the main question of Erdős Problem #130 (theorem erdos_130 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/130.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

Let A\subset\mathbb{R}^2 be an infinite set which contains no three points on a line and no four points on a circle. Consider the graph with vertices the points in A, where two vertices are joined by an edge if and only if they are an integer distance apart. How large can the chromatic number and clique number of this graph be? In particular, can the chromatic number be infinite? The chromatic number can be infinite: there is an infinite general-position set whose integer-distance graph admits no finite proper colouring. How large the *clique* number can be is not addressed here.

Verdict: no verdict yet

formal-conjectures marks problem #130 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.