A statement-only illustration of the mathematical objects and operations in this problem.
Contents
Problem. Determine the largest subset \(A\subseteq\{0,\ldots,9\}^2\) such that no two distinct unordered pairs of points in \(A\) determine parallel segments.
Current status (The maximum lies between 10 and 15). A new 10-point witness improves the lower bound, while the complete direction count gives 15.[4]
1Packet records
3 records
Record
Kind
Assessment
A new 10-point witness improves the lower bound, while the complete direction count gives 15.
Result
Evidence: Reproduced
A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1
A new 10-point witness improves the lower bound, while the complete direction count gives 15.[4]
Relevance to this problem
For Most lattice points with all pairwise slopes distinct in a ten by ten grid, record dstg-claim-certified-interval-10-15 (“The maximum lies between 10 and 15”) records a bound, answer, status fact, or structural consequence. The record states: A new 10-point witness improves the lower bound, while the complete direction count gives 15.
Evidence
ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope.
Record state
established
Scope
all subsets of the 10 by 10 lattice grid with pairwise distinct undirected slopes
Let \(M_{10}\) denote the maximum. The point set
\[
A=\{(0,7),(1,2),(2,0),(4,6),(5,3),(6,9),(7,1),(8,1),(9,5),(9,8)\}
\]
has ten points. Reducing every difference vector by the greatest common divisor of its coordinates, with a fixed sign convention, produces 45 distinct primitive directions. Thus \(M_{10}\geq10\).
For the upper bound, every segment direction has a unique representative \((a,b)\) with \(0\leq a\leq9\), \(-9\leq b\leq9\), \(\gcd(a,|b|)=1\), and \(a>0\), apart from the vertical representative \((0,1)\). Exact enumeration gives 112 supported undirected directions. A \(k\)-point set in the problem uses a different direction for each of its \(\binom{k}{2}\) pairs, so
\[
\binom{k}{2}\leq112.
\]
Since \(\binom{15}{2}=105\) and \(\binom{16}{2}=120\), this proves \(M_{10}\leq15\). The certified interval is therefore
\[
\boxed{10\leq M_{10}\leq15}.
\]
The exact value remains unresolved in this entry.
The literature confirms the established problem family, while the capped size-11 run returned no certificate.
Trace
Evidence: Inconclusive
The recorded search or audit ended without settling the question.
attempt · Route 1
The literature confirms the established problem family, while the capped size-11 run returned no certificate.[1][2][3][4]
Relevance to this problem
For Most lattice points with all pairwise slopes distinct in a ten by ten grid, record dstg-attempt-literature-and-size-eleven-audit (“The finite gap remains open after the source and solver audit”) documents a concrete method, search boundary, or failed route. The record states: The literature confirms the established problem family, while the capped size-11 run returned no certificate.
Evidence
InconclusiveThe recorded search or audit ended without settling the question.
Scope
literature on distinct-slope grid sets and a timeboxed size-11 satisfiability search for the 10 by 10 grid
Erdős, Graham, Ruzsa, and Taylor introduced the grid function in 1992 and proved asymptotic lower and upper bounds. Zhang improved the lower bound in 1993. Clemen's 2026 paper gives the current asymptotic lower bound
\[
g(n)=\Omega\left(\frac{n^{2/3}(\log\log n)^{1/3}}{(\log n)^{1/3}}\right).
\]
These asymptotic results do not settle the ten-grid instance.
Peile and Taylor studied exactly the rectangular finite problem in 2000. The publisher abstract says that values or bounds are supplied for \(m\leq n\leq11\), but the accessible metadata does not expose the table entry for \(d(10,10)\). This audit therefore records the paper without attributing a numerical result that could not be checked.
Distinct-difference configurations and Costas arrays are nearby but weaker for this purpose. They forbid repeated displacement vectors. Two parallel segments of different lengths can satisfy that condition, while the present problem forbids them.
For a direct exact test, Z3 5.0.0 was given 100 selection variables, an exact cardinality of 11, one pseudo-Boolean at-most-one constraint for each of the 112 direction classes, and the two translation normalizations used by the artifact. The run was stopped after 139 seconds and returned `unknown`; it supplies no upper bound. The artifact gives a solver-independent 0-1 pseudo-Boolean instance for continuing the size-11 case and checking any future certificate.
Standard-library Python checks all slopes, proves the counting bound, and hashes a complete 0-1 pseudo-Boolean instance for the next case.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1
Standard-library Python checks all slopes, proves the counting bound, and hashes a complete 0-1 pseudo-Boolean instance for the next case.[4]
Relevance to this problem
For Most lattice points with all pairwise slopes distinct in a ten by ten grid, record dstg-artifact-witness-direction-check (“Exact witness verifier and size-11 continuation instance”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks all slopes, proves the counting bound, and hashes a complete 0-1 pseudo-Boolean instance for the next case.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
the displayed 10-point witness, all 45 of its pairs, all 4,950 grid pairs, and a canonical pseudo-Boolean continuation instance
join source_lines with newline and run with python3
Runtime
CPython 3, standard library only
Details
The program represents an undirected slope by a sign-normalized primitive integer pair. It checks every one of the witness's 45 pairs and enumerates the complete set of 112 directions supported by the grid.
It also constructs a precise continuation for testing size 11. A Boolean variable selects each grid point. For each two point-pairs with the same direction, a three-variable or four-variable inequality forbids selecting their union. The program deduplicates these to 331,537 conflict constraints. It adds the cardinality target \(\sum x_i\geq11\). Two safe translation constraints require a selected point on the left edge and one on the bottom edge, since any solution can be translated until its minimum coordinates are zero. The resulting canonical pseudo-Boolean text has SHA-256 digest `4f61cab88ff8fbabfc4ee3165bba3bb486f4f874c799cd9a4ebf0fee4d8ec93b`.
Original intake status. OPEN in the reviewed TheoremDB packet as of 2026-08-01. A new 10-point witness improves the lower bound, while the complete direction count gives 15.
Store each used slope as a normalized primitive pair (a,b) with a>0, or a=0 and b>0. Adding one point must create pairwise new slopes disjoint from the stored set.
The pair-count bound uses all 112 slopes available anywhere in the box and gives size at most 15. Most slope sets cannot be realized simultaneously, so a geometric branch bound should be much sharper.
Translations, reflections, and coordinate exchange can normalize the first points.
Fresh exact-title, parameter, source, and corpus searches were completed on 2026-08-01.
Recorded example 1. A 9-point incumbent is (3,8),(1,1),(0,8),(6,9),(5,5),(1,2),(7,0),(9,4),(8,7).
Computational notes
All primitive undirected directions supported by the grid were enumerated exactly; there are 112. Thirty thousand seeded random greedy runs found the displayed 9-point set, and an exact pair check verified that its 36 slopes are distinct.
How the 3 records connectThe overview places each record once. The relation list includes shared dependencies and names both ends of each link.
ProblemMost lattice points with all pairwise slopes distinct in a ten by ten grid
Contribute to this problemCite this problem statement
Cite the original sources separately.
Plain text
“Most lattice points with all pairwise slopes distinct in a ten by ten grid.” TheoremDB. P2682. Problem statement; statement text SHA-256 a29f150eebb401757e1c1a36d873934f3d387e92d26ebbe0a1c8b20f398aa1f9. https://theoremdb.org/statement/?ref=P2682
BibTeX
@misc{theoremdb-problem-a29f150eebb401757e1c1a36d873934f3d387e92d26ebbe0a1c8b20f398aa1f9,
title = {{Most lattice points with all pairwise slopes distinct in a ten by ten grid}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 a29f150eebb401757e1c1a36d873934f3d387e92d26ebbe0a1c8b20f398aa1f9},
url = {https://theoremdb.org/statement/?ref=P2682}
}
Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
R.E Peile and H Taylor, “Sets of points with pairwise distinct slopes”. Computers & Mathematics with Applications 39(11) (2000), 109-115. DOI 10.1016/S0898-1221(00)00115-2. Source location cited by the reviewed packet record. ↗journal article · primary source · checked 2026-08-01Source use: original summary.Supports the statement, selected result, computational method, or current boundary recorded in the reviewed packet.Also cited at R. E. Peile and H. Taylor, Sets of points with pairwise distinct slopes, Computers & Mathematics with Applications 39 (2000), 109-115; Felix Christian Clemen, Applications of Sparse Hypergraph Colorings, Discrete Mathematics 349 (2026), 114822; solver run on 2026-07-25.For Most lattice points with all pairwise slopes distinct in a ten by ten grid: The literature confirms the established problem family, while the capped size-11 run returned no certificate.
Paul Erdős, Ron Graham, Imre Z. Ruzsa, and Herbert Taylor, “Bounds for arrays of dots with distinct slopes or lengths”. Combinatorica 12(1) (1992), 39-44. DOI 10.1007/BF01191203. Main asymptotic lower and upper bounds on pp. 39-44. ↗journal article · primary source · version of record · checked 2026-07-28Source use: original summary.For Most lattice points with all pairwise slopes distinct in a ten by ten grid: Introduces the grid distinct-slope function and proves its first asymptotic bounds.Introduces the grid distinct-slope function and proves its first asymptotic bounds.
Zhen Zhang, “A note on arrays of dots with distinct slopes”. Combinatorica 13(1) (1993), 127-128. DOI 10.1007/BF01202795. The improved asymptotic lower bound on pp. 127-128. ↗journal article · primary source · version of record · checked 2026-07-28Source use: original summary.For Most lattice points with all pairwise slopes distinct in a ten by ten grid: Improves the lower bound for the distinct-slope grid function.Improves the lower bound for the distinct-slope grid function.
Packet source. Felix Christian Clemen, “Applications of sparse hypergraph colorings”. Discrete Mathematics 349(2) (2026), 114822. DOI 10.1016/j.disc.2025.114822. Full journal article relevant to Most lattice points with all pairwise slopes distinct in a ten by ten grid. ↗open copy ↗scholarly publication · reference source · arXiv:2406.01499, checked 2026-08-01 · checked 2026-08-01Source use: citation only.For Most lattice points with all pairwise slopes distinct in a ten by ten grid, the reviewed source scope is Full journal article relevant to Most lattice points with all pairwise slopes distinct in a ten by ten grid.. The packet makes no inference beyond that cited scope.Also cited at Exact construction and direction-count replay in dstg-artifact-witness-direction-check.Also cited at Inline Python 3 computation executed on 2026-07-25.Source named by the research packet.
Original CC0 finite slope-distinctness target.
Discussion
Loading
Past commenters and subscribers receive notifications when someone comments.
