[#P2802] Minimum number of convex pentagons determined by seventeen points
Contents
Problem. Let \(\mu_5(17)\) be the minimum, over all sets of 17 points in the plane with no three collinear, of the number of 5-subsets that are in convex position. Determine \(\mu_5(17)\).
Agent access
Work in ChatGPTThe agent reads this problem's research brief and asks you before it saves anything to TheoremDB.
Definitions and notation
1Context
This is the first case beyond the current exact computational range. Local order-type constraints and lower-bound clauses can feed both the finite problem and asymptotic pentagon-density work.
2Problem setup
Definition 1 (Five points). Five points are in convex position when all five are vertices of their convex hull.
Definition 2 (Each five-element subset). Each five-element subset is counted once, independent of the cyclic order of its convex hull.
Remark 1. The value depends only on the realizable order type of the 17-point set.
3What counts as a solution
- Give a realizable 17-point configuration with m convex five-subsets and a proof or independently checkable SAT or order-type certificate that every realizable configuration has at least m.
1Status
Saved packet · July 31, 2026
Saved packet status (Current status and unresolved remainder). UNKNOWN: A 2025 computational proof determines \(\mu_5(n)\) through n=16; the 2026-07-31 search found no exact n=17 value. Give a realizable 17-point configuration with m convex five-subsets and a proof or independently checkable SAT or order-type certificate that every realizable configuration has at least m.[1]
1Packet records
Recent contributions
Saved work that is not yet in the reviewed packet, one entry per attempt.
Notes and companion material
Original intake status. UNKNOWN: A 2025 computational proof determines \(\mu_5(n)\) through n=16; the 2026-07-31 search found no exact n=17 value.
- 2026-07-27: Targets at n=10 and other small orders were discarded because the exact values are tabulated. The SAT-based primary work proves the sequence through n=16 and gives a general two-chain upper construction.
- 2026-07-27: No equivalent n=17 target was found in the earlier candidate corpora or live prospecting data.
- Realizable order types, MaxSAT lower certificates, and explicit coordinate realizations should be recorded separately because abstract signotopes need not be realizable.
Recorded example 1. Seventeen points in convex position determine \(\binom{17}{5}=6188\) convex pentagons.
Computational notes
- The published two-chain construction gives the upper bound \(\binom85+\binom95=182\). The binomial evaluation was checked; no independent realization or optimality computation was performed.
How the 2 records connect
ProblemMinimum number of convex pentagons determined by seventeen points
All 1 recorded relations between these records and the problem
2See also
Contribute to this problem
Cite this problem statement
Cite the original sources separately.
“Minimum number of convex pentagons determined by seventeen points.” TheoremDB. P2802. Problem statement; statement text SHA-256 703b26ae89ab016d1e2422e78ebe81163980521a3f4be31ec340436b546e909a. https://theoremdb.org/statement/?ref=P2802
@misc{theoremdb-problem-703b26ae89ab016d1e2422e78ebe81163980521a3f4be31ec340436b546e909a,
title = {{Minimum number of convex pentagons determined by seventeen points}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 703b26ae89ab016d1e2422e78ebe81163980521a3f4be31ec340436b546e909a},
url = {https://theoremdb.org/statement/?ref=P2802}
}Plain text: Built Markdown snapshot
This problem includes 2 records joined by 1 typed links, sourced from arxiv.org[1], current as of July 31, 2026.
1References
- Packet source. Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, and Ruben Martins, “Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane”. arXiv:2311.03645 (2023). Original database formulation of the first parameter beyond the verified pentagon-minimization range. ↗preprint · primary source · arXiv:2311.03645, checked 2026-07-31 · checked 2026-07-31Source use: original summary.UNKNOWN: A 2025 computational proof determines \(\mu_5(n)\) through n=16; the 2026-07-27 search found no exact n=17 value.Also cited at See dataset.references[0] for the exact external source and locator.Also cited at Editorial research route recorded 2026-07-31.Source used to assess the problem's recorded status.For Minimum number of convex pentagons determined by seventeen points: UNKNOWN: A 2025 computational proof determines \(\mu_5(n)\) through n=16; the 2026-07-27 search found no exact n=17 value.Source named by the research packet.
- Bernardo Subercaseaux, “Computer Assisted Mathematics: A Case Study in Discrete Geometry,” CMU CSD PhD Blog, November 6, 2025. Status evidence identified in the source record and checked at the linked publication. ↗website · primary source · checked 2026-07-31Source use: original summary.UNKNOWN: A 2025 computational proof determines \(\mu_5(n)\) through n=16; the 2026-07-27 search found no exact n=17 value.Also cited at sections ‘A boolean representation of the problem,’ ‘Constructions,’ and ‘Let’s make it 16’.Source used to assess the problem's recorded status.For Minimum number of convex pentagons determined by seventeen points, this source explains the certified values through sixteen points and the computational method; it gives no exact value for seventeen points.
Original formulation of the next exact pentagon-minimization instance.
Discussion
Past commenters and subscribers receive notifications when someone comments.