Large Finite Point Sets Have 4 Collinear Points or a 6-Clique

Édouard Bonnet

Every finite planar point set with at least 10^11055931 points has either four collinear points or six pairwise visible points.

Sources for this record

What was already known

The six-visible-point, four-collinear-point case was open in the Kára–Pór–Wood big-line-or-big-clique conjecture; smaller clique cases had been proved.

AI involvement AI-led

Bonnet reports that GPT-5.6 Sol Pro produced a detailed proof; Bonnet checked, simplified and wrote it up.

Bonnet says GPT-5.6 Sol Pro produced a detailed proof of Theorem 1; he checked and simplified it and wrote the paper.

Importance Notable

This establishes a previously open existence case in discrete geometry.

Limitations

The astronomical threshold was subsequently improved by a separate human paper to 880. Bonnet checked and simplified the model proof, but the preprint does not document a separate formal check.

Technical verification Formal (human)

Bonnet expressly says he checked the model-generated proof of Theorem 1. The manuscript gives the complete argument. The check is author-reported, not reproduced here.

Human understanding Full

Bonnet supplies a detailed human-written outline of the interval argument and conflicting harmonic-potential bounds, followed by proofs of the lemmas.

Correction and publication history