TheoremDB
R373attemptStatus: next experimentEvidence: ReportedReplay: source only

[#R373] Run the unrestricted Sudermann-Merx global model at n = 10

View evidenceOpen source ↗

1Summary

Pin the public model and exact incumbent, retain only proved symmetry reductions, and export enough solver state for independent interval or rational checking.

Use companion repository commit \(4e725664b35a6e5640876e56b1cd0ec3aeeef6e5\) and set \(n=10\) in \(optimization_models/heilbronn_final.py\). Seed the exact Comellas–Yebra coordinates and value as the incumbent. Retain the proved five-boundary-point canonicalization from Proposition 2. Run the full \(P_\Delta^*\) model over arbitrary ten-point configurations. Leave out the Monji-Modir-Kocuk two-points-per-edge conjecture and \(y_5\le1/2\) restriction.

A first budget is 24 wall-clock hours with at most 16 threads and 64 GiB RAM. Record Python, Gurobi, operating system, CPU, model parameters, deterministic seed, primal and dual bounds, node counts, logs, checkpoints, and the final solver status. Export each incumbent as exact decimal strings and save every certificate or box description needed for independent interval or rational checking.

Reported evidence. Recorded scope: all configurations of ten distinct points in the unit square, without structural symmetry or boundary-pattern assumptions.

2Outcome

Evidence package: source only

A verification source is cited. This record has no executable replay attached.

Verification source: github.com ↗, Plan checked against theoremdb on 2026-07-28; model and repository audited at the pinned public commit

3Overview

A universal upper bound of 0.04654 is a useful intermediate result. A timeout or resource limit should become an explicit attempt record with its last certified upper bound. Keep the problem open until a universal exact or rigorous interval upper bound matches the exact construction value.

4What was measured

Check plan impression id
tdbri2:5c42aeb60063792b2e839850959aec96bb9476aa968f23b587658874ebc567db
Check plan response sha256
210dc5c0c5f573e9f4e5270276f5c05c959f57bb04b09ae2d0e8ae8fb82613b5
Duplicate risk
low
Prior record count
0
Stop conditions
matching universal upper bound certified, 24-hour wall-clock budget exhausted, 64 GiB memory budget exhausted, solver or license failure
Required outputs
exact environment and solver version, model parameters and deterministic seed, complete solver log, checkpoint files, incumbent coordinates and objective, time series of primal and certified dual bounds, node counts and final status, upper-bound or box certificates suitable for independent checking

Resources

initial wall clock hours24maximum threads16memory gib64solverGurobi 11 or newersolver licenseproprietary; user-supplied license requiredpython3.9 or newerstorageallow at least 20 GiB for logs, checkpoints, model exports, and certificates

Acceptance

intermediate universal upper bound0.047final upper bound target5*z^2/8 - z^3/2 with 12*z^3 - 27*z^2 + 20*z - 4 = 0exact lower bound decimal 400.04653741958254177256161176810014551328871required scopeunrestricted ten-point configurationsindependent checkrational or outward-rounded interval verification of every primal configuration and any final upper-bound certificatecanonical resolution conditiona universal exact or rigorous interval upper bound matching the exact construction

5How it connects

Recorded for

6Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R373",
  "content_hash": null,
  "slug": "heilbronn10-attempt-unrestricted-global-certificate",
  "type": "attempt",
  "title": "Run the unrestricted Sudermann-Merx global model at n = 10",
  "summary": "Pin the public model and exact incumbent, retain only proved symmetry reductions, and export enough solver state for independent interval or rational checking.",
  "relevance": "For Exact ten-point Heilbronn number in the unit square, record heilbronn10-attempt-unrestricted-global-certificate (“Run the unrestricted Sudermann-Merx global model at n = 10”) documents a concrete method, search boundary, or failed route. The record states: Pin the public model and exact incumbent, retain only proved symmetry reductions, and export enough solver state for independent interval or rational checking.",
  "relevance_source": "recorded",
  "body": "Use companion repository commit \\(4e725664b35a6e5640876e56b1cd0ec3aeeef6e5\\) and set \\(n=10\\) in \\(optimization_models/heilbronn_final.py\\). Seed the exact Comellas–Yebra coordinates and value as the incumbent. Retain the proved five-boundary-point canonicalization from Proposition 2. Run the full \\(P_\\Delta^*\\) model over arbitrary ten-point configurations. Leave out the Monji-Modir-Kocuk two-points-per-edge conjecture and \\(y_5\\le1/2\\) restriction.\n\nA first budget is 24 wall-clock hours with at most 16 threads and 64 GiB RAM. Record Python, Gurobi, operating system, CPU, model parameters, deterministic seed, primal and dual bounds, node counts, logs, checkpoints, and the final solver status. Export each incumbent as exact decimal strings and save every certificate or box description needed for independent interval or rational checking.\n\nA universal upper bound of 0.04654 is a useful intermediate result. A timeout or resource limit should become an explicit attempt record with its last certified upper bound. Keep the problem open until a universal exact or rigorous interval upper bound matches the exact construction value.",
  "status": "next_experiment",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "universal",
    "statement": "all configurations of ten distinct points in the unit square, without structural symmetry or boundary-pattern assumptions"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://github.com/spiralulam/heilbronn/tree/4e725664b35a6e5640876e56b1cd0ec3aeeef6e5",
      "locator": "Plan checked against theoremdb on 2026-07-28; model and repository audited at the pinned public commit"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://github.com/spiralulam/heilbronn/tree/4e725664b35a6e5640876e56b1cd0ec3aeeef6e5",
    "locator": "Plan checked against theoremdb on 2026-07-28; model and repository audited at the pinned public commit"
  },
  "relations": [
    {
      "slug": "R371",
      "title": "Audit the live record, primary sources, and current arXiv frontier",
      "object_type": "attempt",
      "relation": "constrains",
      "direction": "incoming"
    },
    {
      "slug": "R375",
      "title": "The best-known ten-point area is 0.0465374195825..., with global optimality open",
      "object_type": "claim",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R374",
      "title": "The exact Comellas–Yebra construction has minimum area 0.0465374195825...",
      "object_type": "claim",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R376",
      "title": "The Comellas–Yebra three-parameter family has exact maximum 0.0465374195825...",
      "object_type": "claim",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R372",
      "title": "Cover the symmetric family by exact determinant intervals",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "heilbronn-square-ten",
      "title": "heilbronn square ten",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

7Provenance

View source, identifiers, and projection details
Project
heilbronn-square-ten-research
Locator
Plan checked against theoremdb on 2026-07-28; model and repository audited at the pinned public commit
License
CC0-1.0
Public record
R373
Stable alias
heilbronn10-attempt-unrestricted-global-certificate
Projection
Reproduction fields are derived from the immutable record.

A route someone took, recorded so the next person can reuse it or avoid it.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.