# P2802: Minimum number of convex pentagons determined by seventeen points

- ID: `P2802`
- Reference: `minimum-convex-pentagons-seventeen`
- Page: https://theoremdb.org/statements/P2802
- Record maturity: Reviewed problem with recorded work

## 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)\).

### Problem setup

- **Definition.** Five points are in convex position when all five are vertices of their convex hull.
- **Convention.** Each five-element subset is counted once, independent of the cyclic order of its convex hull.
- **Remark.** The value depends only on the realizable order type of the 17-point set.

### What 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.

## Status

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](#reference-1)

## Work

### Evidence for the current status

**Claim 1 (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.

UNKNOWN: A 2025 computational proof determines \(\mu_5(n)\) through n=16; the 2026-07-31 search found no exact n=17 value.

A complete resolution must satisfy this condition: 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.

### Background and intake notes

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.

- Original intake status: UNKNOWN: A 2025 computational proof determines \(\mu_5(n)\) through n=16; the 2026-07-27 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: Seventeen points in convex position determine \(\binom{17}{5}=6188\) convex pentagons.

### Open directions

- **Route 1** (reported): 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](#reference-1)

### 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.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `minimum-convex-pentagons-seventeen`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## References

1. <a id="reference-1"></a>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 https://arxiv.org/abs/2311.03645
   - Also cited at See dataset.references[0] for the exact external source and locator.
   - Also cited at Editorial research route recorded 2026-07-31
   - preprint; reference source; arXiv:2311.03645, checked 2026-07-31; checked 2026-07-31
   - Source use: citation_only
   - 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.
2. <a id="reference-2"></a>Bernardo Subercaseaux, “Computer Assisted Mathematics: A Case Study in Discrete Geometry,” CMU CSD PhD Blog, November 6, 2025. sections ‘A boolean representation of the problem,’ ‘Constructions,’ and ‘Let’s make it 16’ https://www.cs.cmu.edu/~csd-phd-blog/2025/sat-for-math/
   - website; reference source; checked 2026-07-31
   - Source use: citation_only
   - 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.