Browse › Combinatorics › 183 Power savings for planar halving lines and k-sets
A power saving for planar halving lines
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
There are absolute constants ε > 0 and C such that every sufficiently large even n-point set in the plane with no three collinear has at most $Cn^{4/3-\varepsilon}$ unordered halving pairs. This gives a power saving over the classical $O(n^{4/3})$ bound for planar halving lines. The proof is nonquantitative and does not supply explicit constants.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI, Power savings for planar halving lines and k-sets: Lean scope notes (OpenAI mathematics release, lean/docs/183.md, 2026-10-06). The release's formalization covers the $Cn^{4/3-\varepsilon}$ halving-pair bound (Theorem 1.1) and the switch bound under the generic-position assumptions (Theorem 1.2), with existential constants; the $k$-set corollary is not in scope. [family-level]
- OpenAI, HalvingLines.lean comparator challenge (openai/math, commit adc7f12). Comparator statement file: a single theorem
power_boundsthat states both the halving-pair bound and the switch-count bound, left assorryand checked against the release's separate proof. [family-level] - anxkhn, feat(Paper): add the planar halving-line power saving (google-deepmind/formal-conjectures PR #6979, 8–11 October 2026). Independent PR adding the Theorem 1.1 statement to formal-conjectures with a bridge to the first conjunct of the pinned OpenAI
power_boundsproof; reviewer bocowgill confirmed the statement matches Theorem 1.1 and approved on 11 October after running Comparator independently (with small Lean/Mathlib version adaptations). [AI-generated per source] - anxkhn, Add the power-saving upper bound for planar halving lines (google-deepmind/formal-conjectures issue #6974, 8 October 2026). Tracking issue for the PR above, restricted to halving pairs; the author discloses AI assistance (OpenCode using GPT-6.1 Sol). [AI-generated per source]
Possibly relevant literature (found by the agent, not checked)
- Tamaki and Tokuyama, A Characterization of Planar Graphs by Pseudo-Line Arrangements (Algorithmica 35(3):269–285, 2003). Shows that Dey's $O(nk^{1/3})$ level bound also holds for pseudoline arrangements, which bears on the paper's remark that Corollary 1.3 "asserts no corresponding saving for pseudolines".
Digests and expositions
- Open Mathematics Courses / Claude Opus 5.5, Results on halving lines and k-sets: the theorems, Dey's bound, the packing estimate and the tools of its proof, with their assumptions (Open Mathematics Courses, undated). Guide linking lessons on the paper's rank sweeps, activity-packing argument, spatial limits and $k$-set conclusion; it states the lessons were written and self-checked by AI without completed independent mathematical review. [AI-generated per source]
- heyprof, Halving lines and k-sets – interactive explanation (heyprof, undated). Interactive exposition illustrating halving lines and rotating-line switches, comparing counts with Dey's bound, and discussing family 183's claimed exponent improvement with unspecified constants. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 183
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:A-power-saving-for-planar-halving-lines-September-25-2026,
author = {{OpenAI}},
title = {{A power saving for planar halving lines}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/A-power-saving-for-planar-halving-lines-September-25-2026/main.pdf}{OAI:A-power-saving-for-planar-halving-lines-September-25-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/183.md. The Lean statements have not been checked by people against the paper's claims.
Family 183: Power savings for planar halving lines and k-sets
Improves the planar halving-line bound to $O(n^{4/3-\varepsilon})$ for sets with no three collinear and an absolute ε > 0. More generally, an n-point set with no three collinear has $O(n(k+1)^{1/3-\varepsilon_0})$ strictly separable k-subsets for $1\le k\le n/2$, with an absolute $\varepsilon_0\gt 0$. The constants and positive exponents are nonquantitative.
This is the only paper in this family.