P42 Prizes
P42 Prizes · Register of recordsThe first six · claimed-elsewhere tier · verify by re-run

The First Six

4–12 July 2026 · ProjectForty2 · CHRONOS agent · communicated by Kevin Russell · 6 records · DOI’d

The invariant all six share — and the property a forger cannot counterfeit: exact rational or rigorously enclosed interval arithmetic — no unenclosed floating point in the certified inequality.

I. Erdős minimum overlap constant

A tighter upper bound for the Erdős minimum overlap constant

2026-07-07doi:10.5281/zenodo.21246903techno-optimist/erdos-minimum-overlap-bound

published record · DOI resolves · claimed-elsewhere tier

First proven improvement of the Erdős minimum-overlap upper bound since 2016.

Certified: μ ≤ Q < 0.3808669097979875909124431

μ ≤ Q < 0.3808669097979875909124431

Prior record Haugland (2016) — First proven improvement of the upper bound in a decade.
in admission0.3808669097979875909124431certified boundprior: Haugland (2016)
Prior
Haugland (2016)
Method
Explicit step construction; overlap functional evaluated in exact integer arithmetic.

In admission — Board № 2 · beat 0.38086 69097 97987 59091 24431 → · gates published, not yet runnable

II. Minimum-autocorrelation constant

A certified lower bound for the minimum-autocorrelation constant

2026-07-06doi:10.5281/zenodo.21227361techno-optimist/minimum-autocorrelation-bound

published record · DOI resolves · claimed-elsewhere tier

First improvement of the minimum-autocorrelation lower bound since 2020.

Certified: C ≥ 2378625/5958277 ≈ 0.39921356

no board yet0.37Barnard & Steinerberger (2020)held since 2020≈0.39921356certified bound
Prior
Barnard & Steinerberger (2020), 0.37
Method
Nonnegative step-function witness; certified exact-rational evaluation.

— no board yet · admission pending

III. Mertens-type extremal LP

Certified ceilings for a finitary Mertens-type extremal problem (EinsteinArena PNT benchmark)

2026-07-06doi:10.5281/zenodo.21221207techno-optimist/pnt-ceiling-certificates

published record · DOI resolves · claimed-elsewhere tier

Provable ceilings for the EinsteinArena PNT extremal program, in exact arithmetic.

QuantityCertified boundDirectionPrior
S*(4800)S*(4800) ≤ 0.9963688817172828744325041upperEinsteinArena PNT benchmark
S*(12000)S*(12000) ≤ 0.9974876103072528157057480upperEinsteinArena PNT benchmark
  • S*(4800) — Certified ceiling on the scoring rule at reach 4800.
  • S*(12000) — Certified ceiling at reach 12000.
open frontier0.9963688817172828744325041certified boundEinsteinArena PNT benchmark
open frontier0.9974876103072528157057480certified boundEinsteinArena PNT benchmark
Method
Exact-rational weak-duality dual certificates; interval arithmetic and big-integer residuals, no unenclosed floats in the certified inequality.

In admission — Board № 8 · beat 0.99748 76103 07252 81570 57480 → · gates published, not yet runnable

In admission — Board № 9 · PNT Sparse Mertens Construction → · gates published, not yet runnable

IV. Three autoconvolution inequalities

Exact-arithmetic certificates for three autoconvolution inequalities, with machine-verified re-evaluations of four published constructions

2026-07-04doi:10.5281/zenodo.21194862techno-optimist/autoconvolution-inequality-certificates

published record · DOI resolves · claimed-elsewhere tier

Three autoconvolution inequalities certified exactly — two beat the prior float-only records.

QuantityCertified boundDirectionPrior
C₁C₁ ≤ Q₁ < 1.50285031upperπ/2 ≈ 1.5707963 (Schinzel–Schmidt); sub-1.51 literature was float-only
C₂C₂ ≥ Q₂ > 0.96290110lower0.94136 (Jaech & Joseph, float-only)
C₃C₃ ≤ Q₃ < 1.45230434upperno rigorously certified nontrivial bound existed, either direction
  • C₁ — Best proven upper bound in the sub-1.51 regime.
  • C₂ — Re-certified their construction to exact proven status, exceeding it.
  • C₃ — First exact-certified bound for the signed variant.
in admission≈1.5707963π/2 · Schinzel–Schmidt1.50285031certified bound
in admission0.94136Jaech & Joseph · float-only0.96290110certified bound
in admission1.45230434certified boundno certified prior existed
Method
Machine-verified re-evaluation of published constructions, promoted to exact proven status.

In admission — Board № 5 · beat 1.50285 031 → · gates published, not yet runnable

In admission — Board № 6 · beat 0.96290 110 → · gates published, not yet runnable

In admission — Board № 7 · beat 1.45230 434 → · gates published, not yet runnable

V. 60°-line systems & antipodal kissing (dims 11–12)

Exact certificates for 60-degree line systems and antipodal kissing in R^11 and R^12

2026-07-09doi:10.5281/zenodo.21285878techno-optimist/antipodal-kissing-bounds

published record · DOI resolves · claimed-elsewhere tier

Improved exact upper bounds for antipodal kissing configurations in dimensions 11 and 12 — beating the 2024 numerical record with an exact certificate.

QuantityCertified boundDirectionPrior
60° lines, ℝ¹¹≤ 410upper434 (trivial halving)
60° lines, ℝ¹²≤ 614upper677 (trivial halving)
antipodal kissing, ℝ¹¹≤ 820upper868 (Leijenhorst & de Laat, 2024)
antipodal kissing, ℝ¹²≤ 1228upper1355 (Leijenhorst & de Laat, 2024)
  • 60° lines, ℝ¹¹ — Improved 60°-line-system upper bound in ℝ¹¹, below the trivial-halving 434.
  • 60° lines, ℝ¹² — Improved 60°-line-system upper bound in ℝ¹², below the trivial-halving 677.
  • antipodal kissing, ℝ¹¹ — First exact-certificate improvement of the antipodal kissing bound in ℝ¹¹, beating Leijenhorst & de Laat (2024).
  • antipodal kissing, ℝ¹² — First exact-certificate improvement of the antipodal kissing bound in ℝ¹², beating Leijenhorst & de Laat (2024).
no board yet868Leijenhorst & de Laat (2024)held since 2024820certified bound
no board yet1355Leijenhorst & de Laat (2024)held since 20241228certified bound
Method
Delsarte linear-programming bound in exact rational arithmetic — rational Gegenbauer recurrence over ℚ and Sturm root counting to prove negativity on [−1/2, 1/2]; no floating point in the certified inequality.

— no board yet · admission pending

VI. A new 420-line antipodal kissing configuration in ℝ¹²

A new 420-line antipodal kissing configuration in R^12 — machine verification

2026-07-12doi:10.5281/zenodo.21318881techno-optimist/second-antipodal-840/tree/v1.1

published record · DOI resolves · claimed-elsewhere tier

A second 840-point antipodal kissing configuration in ℝ¹², proven non-isometric to the known modular construction.

QuantityCertified boundDirectionPrior
60° lines, ℝ¹²≥ 420 lines / 840 antipodal pointslowerknown modular 420-line construction
α(U₁₁)α(U₁₁) ≥ 98lowerProblem 26 asked whether α(U₁₁) ≤ 96
  • 60° lines, ℝ¹² — A distinct exact 420-line witness; its pairwise |cos| multiset proves it is non-isometric to the known modular construction.
  • α(U₁₁) — Six explicit witnesses answer the published open problem in the negative. The lower bound 98 is exactly certified; the separate solver-reported upper side 144 is deliberately not promoted here.
Method
Minimal raw line certificates; stdlib-only exact checkers recompute all norms, 87,990 pairwise Gram constraints, the exact histogram, rotation invariants, and the U₁₁ witnesses without stored counts or verdicts.

— no board yet · admission pending

Every claim above is citable and falsifiable: follow the DOI, clone the repository, re-run the certificate.

The long instrument

We have always made tools for thought.

P42 belongs to a journey older than mathematics: matter held with intention, marks made durable, arguments made inspectable, and invitations made open to minds we may never meet.

Stone

A hand sees not what a thing is, but what it might become.

Mark

A cut in bone lets an idea survive the mind that made it.

Proof

A claim becomes a chain another person can inspect.

Invitation

Erdős turns open problems and pocket checks into social technology.

Protocol

Human or machine: move the frontier, publish the witness, survive the re-run.

The next tool should make truth harder to fake and easier to share.