Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to Problem 193 is no. Stijn Cambie and Erik Kalviainen construct an infinite sequence of distinct points with no three collinear whose successive differences lie in , with at most sixteen distinct differences occurring; the finite set of those differences is a step set whose infinite -walk contains no collinear triple. Writing for the binary digit sum of , the planar part of is twice the Gaussian-integer sum shifted by one of four corner offsets chosen by , and the height is . The proof rests on the identity that the -adic valuation of the squared planar chord length between two points equals that of their height difference; three collinear points would give two positive height gaps and with , which is impossible. The two-page argument is elementary and unconditional; the work was AI-assisted, with OpenAI GPT-5.6 Sol named on the claim, and no AI output or finite computation is a premise. The corpus's complete reconstruction of the proof is [[../library/discrete_geometry/cambie_kalviainen_2026_small_step_walk/theorem_1|Theorem 1]] of the source card.
Submission note. Posted to erdosproblems.com as a proof claim by Stijn Cambie, Erik Kalviainen (account ekalvi) on 3 September 2026, giving "OpenAI GPT-5.6 Sol" as the AI used, which the site marks as accepted as correct:
An infinite walk exists from a Gaussian-integer construction. Let count the s in the binary expansion of , and set . Define
Only sixteen step vectors occur.
We prove the key identity
If three points
were collinear, and and were their two consecutive positive height gaps, the identity would force . This is impossible because, after removing their common power of two, and are odd while is even. Notes: This supersedes the exposition, but not the validity, of my earlier Hilbert proof claim. The new joint paper gives a substantially simpler Gaussian-integer construction. Both authors have read, checked, and affirm the unconditional proof. The work was AI-assisted; neither AI output nor finite computation is a premise.
Acceptance. Thomas Bloom, the site's curator, agreed in the claim's thread on 2026-09-03 that the problem should be marked solved and confirmed the update on 2026-09-04; the problem page credits the negative answer to Cambie and Kalviainen. Those comments concern this joint proof, posted to the site as proof claim 239 two days after the arXiv submission of 2026-09-01. No journal publication was found in the status search. The corpus's own review of the reconstruction, recorded on the source card, is not acceptance evidence here.
Formalization. The authors' repository, linked above at its pinned
commit, holds a Lean 4 development that declares itself a formalization of
this Gaussian-integer proof; its main theorem is
Hilbert193.erdos193_unconditional, and the package keeps the historical
Hilbert193 name from the earlier Hilbert-curve development, which it
replaced on 2026-09-01 and which is recorded on
its own claim page.
This corpus has not built or audited the development, so it is not listed as
evidence.