Minimum spanning-tree dilation on the regular nonagon

TheoremDB P2502 · computational geometry

Source catalogue assessmentAs of 2026-09-08Source & evidence ↓

Read original source ↗ 0 Submit progress Lean 4 ↓Discussion (0)

Problem statement

Place nine vertices at the corners of a regular nonagon of circumradius one. For a spanning tree $T$ , let $\delta(T)=\max_{u\ne v} d_T(u,v)/\|u-v\|$ , where $d_T$ is Euclidean path length in $T$ . Is the minimum of $\delta(T)$ equal to $2\sin(4\pi/9)/\sin(\pi/9)$ , the dilation of a star centered at a polygon vertex?

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Share a formalization →Verification guide ↗

Progress & source assessment

Source-reported assessment, retrieved 8 September 2026. Frontier Science has not independently reviewed this status.

Resolved. Not Lean-verified

References

[1]TheoremDB P2502 link

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.