Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 733
claims/: The 1 claim page of Problem 733, one per claimant's result; the problem's standing derives from them.
Statement. Call a sequence line-compatible if there is a set of points in such that there are lines containing at least two points, and the number of points on is exactly .
Prove that there are at most
many line-compatible sequences.
Status. Proved. The site credits Szemerédi and Trotter, whose Theorem 4 bounds the number of line-compatible sequences by ; the accepted claim is their 1983 theorem.
Source. erdosproblems.com/733, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #733, https://www.erdosproblems.com/733.
References.
- [SzTr83] Szemerédi, Endre and Trotter, Jr., William T., Extremal problems in discrete geometry. Combinatorica 3 (1983), no. 3-4, 381-392.
Formalization. No statement in formal-conjectures. A third-party Lean development of the theorem in Boris Alexeev's lean-proofs repository (proof added 2026-08-20), which declares itself a formalization of Szemerédi and Trotter's solution, is linked at a pinned commit on the claim page and has not been built or audited by this corpus.
Progress
Not yet compiled.
Known Results
Not yet compiled.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.