files / notes / picks / 2026-08-16-judge-codex.md

18 KB · on GitHub

Codex judge ballot — overnight picks

I score the proposed first quest, not the fame of the parent problem. A finite computation that merely illustrates a conjecture is not a dent; the output must be a new exact witness, a certified finite obstruction, or a strict numerical bound improvement.

P01. Quantitative arithmetic removal in the integers

P02. A logarithmic saving for five-term progression-free sets

P03. Four-term progressions in Fourier-uniform sets

P04. The Möbius-ladder Cayley–Sidorenko inequality

P05. Extremal affine copies of {0,1,3}\{0,1,3\}

P06. Sumsets with no uniquely represented element

P07. The second term for Sidon subsets of [N][N]

P08. A long gap in a dilate modulo a prime

P09. Thin cyclic additive bases

P10. A polynomial-size core in an approximate group

P11. A composite in a sumset below the square-root threshold

P12. Two smooth summands for every integer

P13. Positive density of the Hofstadter ab−1ab-1 closure

P14. A smaller constant in the two-squares gap

P15. Chowla's cosine problem

P16. Zeros of integer cosine sums

P17. Irreducibility of random 0/10/1 polynomials

P18. Close the worst-case trace-reconstruction gap

P19. Full asymptotics for the nn-queens count

P20. Density of the Ulam sequence

P21. Shannon capacity of the 7-cycle

P22. Density loss for linear radius-two covering codes

P23. The first open no-three-in-line grid regime

P24. Cubic stability for large finite-field arcs

P25. Improve the Heilbronn triangle exponent

P26. Carbery's large rectangle problem

P27. Exact Cohn–Elkies certificate for planar circle packing

P28. The chromatic number of the plane

P29. Shrink the 509-vertex five-chromatic unit-distance graph

P30. The five-dimensional kissing number

P31. Existence of a projective plane of order 12

P32. The missing degree-57 Moore graph

P33. Frankl's union-closed sets conjecture

P34. The 1/31/3–2/32/3 conjecture for posets

P35. The three-sunflower conjecture

P36. Caccetta–Häggkvist for directed triangles

P37. Seymour's second-neighborhood conjecture

P38. Tuza's triangle packing-covering conjecture

P39. Push graph reconstruction beyond 13 vertices

P40. Erdős–Hajnal for the six-vertex path

P41. Determine R(5,5)R(5,5)

P42. Determine the van der Waerden number W(2,7)W(2,7)

P43. Improve the lower bound for the seventh Schur number

P44. Lonely runner for 14 runners

P45. The 33-point Erdős–Szekeres problem

P46. The Brocard–Ramanujan factorial-square equation

P47. Uniqueness of Markov numbers

P48. Amenability of Thompson's group FF

P49. Expansion from random generators of alternating groups

P50. Remove the logarithmic loss in permanent formula lower bounds

Top 8

rank PXX slug dentable shape cost why
1 P43 schur-number-seven-bound 5 finite-cex M Direct SAT construction; one extra integer is a strict bound and the coloring is a tiny exact certificate.
2 P06 no-unique-sum-mod-p 5 small-n-proof S Small-prime minima admit witnesses and checkable UNSAT certificates, with a real Green/arXiv target.
3 P13 hofstadter-ab-minus-one-density 4 small-n-proof S Exact closure parent pointers turn a new finite record into a replayable certificate.
4 P46 brocard-ramanujan-factorial-square 4 atp-smt S Modular nonsquare obstructions can yield a short certified elimination of new infinite residue classes.
5 P42 van-der-waerden-w27 4 finite-cex M A coloring of length 3704 immediately and checkably raises the OEIS-backed lower bound.
6 P29 smaller-five-chromatic-unit-distance-graph 4 finite-cex M Deletion plus SAT can return an exact smaller construction, but depends on obtaining the published graph data.
7 P21 shannon-capacity-c7 4 bound-search M A larger independent set in one graph power is a strict capacity-bound move with an elementary checker.
8 P23 no-three-in-line-grid 4 finite-cex M Coordinates or proof logs are clean, though the current first unresolved finite order must be audited before launch.
  1. P43 — schur-number-seven-bound (M): Encode a shifted-template-seeded seven-color sum-free partition of [1697][1697] in incremental SAT and, if found, emit the coloring with an exhaustive exact verifier.
  2. P06 — no-unique-sum-mod-p (S): Determine the exact minimum size for the first unclassified small primes by symmetry-broken SAT, emitting each extremal set or an independently checkable UNSAT certificate.
  3. P13 — hofstadter-ab-minus-one-density (S): Generate the closure with parent pointers and certify a new maximal covered prefix or finite interval-density record, outputting a replayable derivation DAG for every claimed member.
  4. P46 — brocard-ramanujan-factorial-square (S): Mine a new modulus covering additional residue classes of nn, then certify by exact modular arithmetic that n!+1n!+1 is a nonsquare in every covered class beyond the modulus threshold.
  5. P42 — van-der-waerden-w27 (M): Use symmetry-aware incremental SAT and cyclic-zipper seeds to find a 2-coloring of [3704][3704] with no monochromatic 7-AP, then emit and independently verify the coloring certificate.