Aination Works · Catalog

Statement: Recover the cryptographic method and plaintext of the fourth, 97-character section of Jim Sanborn's 1990 Kryptos sculpture at CIA headquarters. Published cribs: positions 64-69 = BERLIN, 70-74 = CLOCK, 22-25 = EAST, 26-34 = NORTHEAST. The ciphertext is fully public. ↗

community acceptance — Proposed key/method must deterministically transform the 97 ciphertext characters into English plaintext reproducing all four published cribs at the stated positions; final confirmation only via Sanborn/Scheidt or a match to the sealed plaintext.

Progress: Sept 2025: Jarett Kobek and Richard Byrne reconstructed the likely plaintext from Sanborn's mis-donated Smithsonian papers (not released; archive sealed 50 years); Sanborn's archive was auctioned Nov 2025. The encryption method remains unknown; multiple 2025-2026 'AI solved K4' claims do not reproduce the cribs and are rejected by the community.

status checked 2026-09-03 · sources: content.rrauction.com, gist.github.com, en.wikipedia.org

Statement: Decipher Edward Elgar's 87-symbol, 3-line note to Dora Penny (14 July 1897) written in an alphabet of 24 semicircle glyphs (1-3 arcs in 8 orientations). Produce the method and a plaintext consistent with the glyph sequence and with Elgar's known use of the same alphabet elsewhere. ↗

expert panel — Method must map the 87 glyphs to a coherent English (or music-notation) plaintext with a key that is not tuned per position; the Elgar Society / Cipher Mysteries community serves as reviewing panel. Unicity distance of 87 symbols makes proof-by-plaintext weak, so the key must be simple.

Progress: No accepted solution. Elgar Society 2007 competition found all entries arbitrary; Wase (2023) computational study argues it is unlikely a simple substitution of English or Latin; 2024-2025 book claims (Bartlett) and musical-cipher readings remain unaccepted.

status checked 2026-09-03 · sources: en.wikipedia.org, ciphermysteries.com, arxiv.org

Statement: Decipher the 13-symbol cipher in the Zodiac Killer's 20 April 1970 letter, prefaced 'My name is ___'. Any solution must specify a cipher system and key consistent with Zodiac's solved Z408 and Z340 practices. ↗

expert panel — Key must be a plausible Zodiac-style homophonic/substitution system; because the text is too short for statistical proof, acceptance requires corroborating evidence (e.g., name matching an identified suspect via DNA or FBI confirmation).

Progress: Z340 solved Dec 2020 (Oranchak, Blake, Van Eycke). Z13 remains unsolved; 2026 AI-assisted name proposals (e.g., 'Margolus' theory) and Zenodo preprints are unverified; Oranchak notes 13 symbols is below the unicity distance so most proposals cannot be falsified.

note: source changed 2026-10-06: https://en.wikipedia.org/wiki/Zodiac_Killer

status checked 2026-09-03 · sources: en.wikipedia.org, gsnsp.com, zenodo.org

Statement: Decipher the 32-symbol cipher from the Zodiac Killer's 26 June 1970 letter, which accompanied a Phillips 66 map of the Bay Area with a compass rose centred on Mt. Diablo and is said to encode where a bomb was set 'radians and # inches along the radians'. Output: key, plaintext, and the implied map location. ↗

expert panel — Key must produce an English plaintext that, combined with the map, yields a specific location; convincing verification requires physical or archival corroboration since 32 symbols is under the unicity distance.

Progress: Ziraoui's 2021 Lake Tahoe claim was not accepted by the FBI or cipher community; 2026 explorations of magnetic-vs-true-north map variants produced no confirmed location or physical evidence.

status checked 2026-09-03 · sources: en.wikipedia.org, praetorian.com, gsnsp.com

Statement: Decipher Beale papers No. 1 (520 numbers; purported treasure location) and No. 3 (618 numbers; purported list of heirs). Paper No. 2 is a book cipher keyed to the Declaration of Independence; the key texts for 1 and 3 are unknown, and the whole story may be an 1885 hoax by publisher James B. Ward. ↗

program checker — Given a candidate key text, apply the book-cipher rule (number -> first letter of nth word) and check that the output is fluent English; automated language-model scoring over the full 520/618 numbers suffices, as with cipher No. 2.

Progress: No accepted solution as of 2026; ongoing computational analyses (e.g., bealeresearch.com) find non-random digit structure consistent with fabrication; stylometry attributes the pamphlet letters to Ward.

status checked 2026-09-03 · sources: en.wikipedia.org, bealeresearch.com, amusingplanet.com

Statement: Produce a reproducible decipherment (or a rigorous proof of meaninglessness) of the c.1404-1438 Voynich manuscript: ~240 vellum pages, ~170,000 glyphs in an unknown script, with full high-resolution scans and machine-readable transcriptions (EVA/IVTFF) public. ↗

expert panel — A candidate key/grammar must be applied mechanically to the public IVTFF transcription and yield coherent, consistent text across many folios (not cherry-picked lines); acceptance via peer review in Cryptologia / Voynich research community.

Progress: No decipherment accepted by scholars as of 2026. Jan 2026 statistical study argues for a cipher rather than a natural language; Bax (2014), Gibbs (2017), Cheshire (2019) and 2025-2026 'AI decoded' claims all rejected for lack of reproducibility across the whole text.

status checked 2026-09-03 · sources: elenigmavoynich.com, archaeologymag.com, voynichlucidity.com, en.wikipedia.org

Statement: Confirm, complete, or refute the decipherment of the Rohonc Codex (448 pages, 87 illustrations, ~792 distinct symbols; Hungarian Academy of Sciences). Király & Tokai (Cryptologia 2018) claim it is a designed code system encoding a Christian devotional text; a full, independently reproducible reading of the whole codex is still lacking. ↗

expert panel — A candidate codebook must be applied to all 448 pages and produce consistent text aligned with the 87 illustrations; independent replication by another team and Cryptologia peer review would constitute acceptance.

Progress: Király & Tokai's 2018 partial decipherment (code system, religious content) is regarded as the most credible progress but has not been extended to a complete, independently verified translation; alternative 2024-2025 proposals (e.g., Old Slavic readings) are speculative.

note: source changed 2026-10-07: http://export.arxiv.org/api/query?search_query=all:Rohonc&sortBy=submittedDate&sortOrder=descending&max_results=10

status checked 2026-09-03 · sources: tandfonline.com, ciphermysteries.com, en.wikipedia.org

Statement: Decipher the two lines of 32 numbers each attributed to Sir Thomas Urquhart (Logopandecteision, 1653) and transmitted via an 1899 biographical source. Any method must be applied mechanically to the numbers and must be consistent with the surviving primary texts (British Library copy, TCP A64608). ↗

expert panel — Run the proposed indexing rule against the TCP transcription of the 32 Proquiritations and check that every one of the 64 numbers yields the claimed letter; additionally the ciphertext's provenance must be traced to a primary source.

Progress: 2026-09-01: Vals AI reported Claude Fable 5.1 solved it in 44 minutes by indexing words in the 32 preceding Proquiritations (plaintext beginning 'O GOD UPHOLD KING CHARLS THE SECOND...'). Same day, reticuli-labs' replication found the distich absent from the 1653 primary sources and that 10 of the required letters cannot be produced by the stated method.

status checked 2026-09-03 · sources: vals.ai, github.com, x.com

Statement: Decipher the 196-character (392-digit) challenge cipher from the first edition of Alexander D'Agapeyeff's 'Codes and Ciphers' (1939), given as 5-digit groups; the author later admitted he had forgotten the method. The ciphertext and the book's worked examples (Polybius-square style) are public. ↗

program checker — Apply the proposed key (square + transposition) to the 392 digits and check that the output is fluent English; a plausible book-style plaintext plus a key describable in a few lines is sufficient, and a hypothesized author error must be minimal and explicit.

Progress: Unsolved; MysteryTwister lists it as a Level X challenge. Ongoing computational analyses (dagapeyeffresearch.com; low index of coincidence 1.812 for digit pairs) support a Polybius-plus-transposition system, possibly with nulls or an enciphering error.

status checked 2026-09-03 · sources: en.wikipedia.org, dagapeyeffresearch.com, mysterytwister.org

Statement: Determine the meaning of the five lines of capital letters (one struck out) pencilled on the back of the Rubaiyat linked to the Somerton Man found dead at Somerton Beach on 1 Dec 1948. The man was identified in 2022 (unofficially) as Carl 'Charles' Webb; the code itself remains unexplained. ↗

expert panel — Any reading must explain all ~50 letters (including the struck line) with a stated rule (e.g., initials of a known text) and ideally match documents from Webb's life; archival corroboration is the only realistic confirmation.

Progress: July 2022: Derek Abbott's team identified the man as Carl Webb via genetic genealogy (not yet officially confirmed by SA Police). Analyses suggest the letters are word initials (possibly horse-racing related); no accepted reading.

status checked 2026-09-03 · sources: en.wikipedia.org, cipherfoundation.org, ciphermysteries.com

Statement: Explain the ten letters 'O U O S V A V V' with 'D M' below, carved on the 18th-century Shepherd's Monument at Shugborough Hall, Staffordshire. A solution must give the intended reading and be historically consistent with the Anson family and the monument's Poussin relief. ↗

expert panel — Only documentary evidence (Anson family papers, 18th-century correspondence) could confirm a reading; with 10 letters no statistical verification is possible.

Progress: No accepted solution; Bletchley Park veterans (2004) and later proposals (Latin initialisms, 'Magdalen' polyalphabetic reading by Ramsden 2014, Edmunds 2016 coordinates) are all unconfirmed. Shugborough Hall reports several new claims weekly.

note: source changed 2026-09-14: https://www.nationaltrust.org.uk/visit/shropshire-staffordshire/shugborough-estate

status checked 2026-09-03 · sources: en.wikipedia.org, npr.org

Statement: Decipher the two handwritten pages of letter/number groups with parentheses found in the pockets of Ricky McCormick (found dead 30 June 1999, Missouri). The FBI's CRRU released images and a public appeal on 29 March 2011; his family disputes that he could write such notes. ↗

expert panel — A consistent expansion rule applied to all groups on both pages yielding coherent English (names, places, dates checkable against the case file) would be evaluated by the FBI CRRU.

Progress: Unsolved since 1999; listed by the FBI as a top unsolved case. Community consensus is that the notes are a personal shorthand (possibly with medical/place-name abbreviations) rather than a formal cipher.

status checked 2026-09-03 · sources: en.wikipedia.org, dcode.fr

Statement: Decipher the 'Blitz Ciphers': handwritten pages in an invented symbol alphabet with geometric diagrams, reportedly found in a bomb-exposed East London cellar after WWII. Eight high-resolution page images and a provisional transcription are public (Cipher Mysteries, 2011-2014); the full set is held privately. ↗

community acceptance — Key must be applied mechanically to the published transcription and produce coherent text across all 8 pages; the owner could confirm on the unpublished pages.

Progress: No decipherment; theories range from homophonic/nomenclator to Masonic or alchemical notation. Limited access to the full corpus (only 8 of many pages) constrains statistical attacks.

status checked 2026-09-03 · sources: ciphermysteries.com, ciphermysteries.com

Statement: Determine R(5,5), the smallest N such that every 2-colouring of the edges of K_N contains a monochromatic K_5. Known: 43 <= R(5,5) <= 46. Concrete subtargets: exhibit a K_5-free 2-colouring of K_43 (would raise the lower bound to 44), or prove R(5,5) <= 45. ↗

program checker — A lower-bound construction is a 2-coloured graph checked for K_5 in O(N^5); an upper-bound proof is a large computer enumeration whose logs/certificates must be independently re-run (gluing of (4,5)- and (3,5)-graphs).

Progress: Angeltveit & McKay proved R(5,5) <= 46 (arXiv Sept 2024, J. Graph Theory 2026), improving 48 (2018). McKay & Radziszowski conjecture R(5,5) = 43; lower bound 43 (Exoo 1989) unchanged.

status checked 2026-09-03 · sources: onlinelibrary.wiley.com, arxiv.org, mathworld.wolfram.com

Statement: Decide whether R(3,10) equals 40 or 41. Equivalently: does there exist a triangle-free graph on 40 vertices with independence number at most 9? If yes, R(3,10)=41; if a full enumeration rules it out, R(3,10)=40. ↗

program checker — A 40-vertex triangle-free graph with alpha <= 9 is checkable in milliseconds; an exhaustive non-existence proof requires re-running a certified enumeration of (3,9)- and (3,10)-graphs.

Progress: Angeltveit (Electronic J. Combin., Nov 2025) proved R(3,10) <= 41, improving Goedgebeur–Radziszowski's 42 (2013); lower bound 40 (Exoo 1989).

status checked 2026-09-03 · sources: combinatorics.org, combinatorics.org

Statement: Determine the maximum number of non-overlapping unit spheres touching a central unit sphere in R^5. Known bounds 40 <= k(5) <= 44. Concrete targets: exhibit 41 unit vectors in R^5 with pairwise angles >= 60 degrees, or prove k(5) <= 43. ↗

program checker — A lower-bound configuration is a list of vectors checked with exact/interval arithmetic for pairwise inner products <= 1/2 (O(n^2)); an upper bound requires a verifiable SDP dual certificate.

Progress: Bounds for dim 5 unchanged (44 upper via de Laat–Leijenhorst SDP, 2024). Nearby records moved: Cohn–Li improved dims 17-21 (2024), AlphaEvolve raised dim 11 to 593 (2025) and 'AI agents in the wild' (Bianchi et al. 2026) to 604; Ho (2026) improved dim 19.

note: STATUS PROPOSAL None (0.55) — data/review/

status checked 2026-09-03 · sources: cohn.mit.edu, phys.org, arxiv.org

Statement: Determine r_3(8), the largest subset of F_3^8 with no three points on an affine line. Exact values are known through dimension 7 (1, 2, 4, 9, 20, 45, 112); in dimension 8 the best construction has 512 points and the exact value is unknown. Target: a cap set of size >= 513 in F_3^8, or a proof that 512 is optimal. ↗

program checker — Check a candidate set for 3-term lines in O(n^2) over F_3^8 (trivial); an optimality proof would need a certified exhaustive search or SAT/ILP certificate.

Progress: FunSearch (DeepMind, Nature, Dec 2023) found a 512-point cap set in dimension 8 (previous 496) and improved the asymptotic lower-bound constant; Tyrrell (2022) and Romera-Paredes et al. hold the asymptotic records. No 2024-2026 improvement in dimension 8 found.

status checked 2026-09-03 · sources: en.wikipedia.org, arxiv.org, arxiv.org

Statement: Construct a 668 x 668 matrix with entries +/-1 and mutually orthogonal rows (H H^T = 668 I). Order 668 was, until Aug 2026, the smallest multiple of 4 for which no Hadamard matrix was known (next: 716, 892, 1132...). The Hadamard conjecture asserts existence for all orders 4k. ↗

program checker — Decode the posted string into a 668x668 +/-1 matrix and check H H^T = 668 I with exact integer arithmetic (O(n^3), seconds); the mathematical claim is thus machine-verifiable and only attribution is disputed.

Progress: 12 Aug 2026: Levent Alpöge (Anthropic) posted a +/-1 string encoding Hadamard matrices for order 668 and 11 other previously unknown orders below 2000, credited to Claude with three human collaborators; Epoch AI marked it 'solved by AI' provisionally pending a full writeup. Earlier: 64-modular Hadamard matrix of order 668 (Australas. J. Combin. 2025). Monitor 2026-09-08: Wikipedia improved prose and citation for August 2026 construction on 2026-09-07. Monitor 2026-09-24: Wikipedia updated Alternative construction section on 2026-09-23

note: progress from source https://en.wikipedia.org/wiki/Hadamard_matrix — verify

status checked 2026-09-03 · sources: epoch.ai, aliteq.com, theoremdb.org

Statement: Extend the exhaustive verification that every n < N reaches 1 under the 3n+1 map. Current certified frontier: all n < 2075 * 2^60 ~ 2^71.02 (Barina, 15 Jan 2025). Target: push the verified bound to 2^72 (or beyond) with reproducible, checkpointed, independently re-runnable code. ↗

program checker — Re-run the open-source sieve-based checker on the claimed range (or a random sample of blocks) and compare per-block checksums with the published logs.

Progress: Barina's distributed project reached 2^71 in Jan 2025 (J. Supercomputing 2025); a Feb 2026 arXiv paper proposes an improved algorithm for checking all n < 2^N. Formalisation efforts continue at ccchallenge.org.

status checked 2026-09-03 · sources: pcbarina.fit.vutbr.cz, github.com, arxiv.org

Statement: Prove that for any 11 runners with distinct constant speeds on a unit circle starting together, each runner is at some time at distance >= 1/11 from all others (k = n-1 = 10 nonzero speeds). The conjecture is proved for up to 10 runners; n = 11 is the smallest open case. ↗

program checker — The method reduces the case to a finite check of integer speed tuples up to an explicit bound (via Tao's reduction); an independent re-run of the enumeration code, or a Lean formalisation, verifies it.

Progress: Rosenfeld proved the 8-runner case (arXiv Sept 2025); Trakulthongchai (Oxford undergraduate) extended computer-assisted proofs to 9 and 10 runners (arXiv Nov 2025, revised Apr 2026) using a sieve refinement.

status checked 2026-09-03 · sources: arxiv.org, arxiv.org, sjc.ox.ac.uk

Statement: Does there exist a composite n with phi(n) | n-1? Known: any such n is odd, squarefree, n > 10^20 (Cohen–Hagis 1980), has omega(n) >= 14 prime factors, and if 3 | n then n > 10^360 and omega(n) >= 40,000,000. Concrete targets: raise the omega(n) lower bound above 14 or the numeric bound above 10^20 with a reproducible search. ↗

program checker — A counterexample is checked instantly (factor n, compute phi); a new lower bound requires re-running the branch-and-bound over prime-factor patterns with published certificates.

Progress: Burek–Żmija (2019) gave the bound n < 2^(2^omega(n)) - 2^(2^omega(n)-1); Pinch's computational notes and a Nov 2025 preprint (unrefereed) discuss 2-adic constraints; no change to the 14-prime bound in 45 years.

status checked 2026-09-03 · sources: en.wikipedia.org, mathworld.wolfram.com, preprints.org

Statement: Does an odd perfect number exist? Known constraints: N > 10^1500 (Ochem–Rao 2012), N has at least 101 prime factors counted with multiplicity and at least 10 distinct primes, largest prime factor > 10^8. Concrete target: extend the certified search to N > 10^2000 or improve a structural constraint. ↗

program checker — Re-run the branch-and-bound factor-chain algorithm with the published prime factorisations (primality certificates needed for large factors); a purported OPN is verified by factoring and summing divisors.

Progress: Ochem–Rao's 10^1500 bound (Math. Comp. 2012) remains the record; ongoing factorisation-based searches (oddperfect.org tradition) and 2023-2025 structural papers (e.g., on the Euler prime and abundancy index) have not changed the headline bound. Monitor 2026-10-01: Bound raised to 115 by Ochem (2026)

status checked 2026-09-03 · sources: mathworld.wolfram.com, researchgate.net, maths-people.anu.edu.au

Statement: For every finite union-closed family of sets (not just {empty}), some element lies in at least half the sets. Proven constant: some element is in at least ~38.2% of sets (Gilmer 2022 gave 1%, improved within weeks to (3-sqrt5)/2 ~ 0.381966, and slightly beyond by Cambie / Liu 2023 / Lu–Raz 2024). Verified by computer for families with <= 50 sets and universes of <= 12 elements. Targets: improve the constant, or extend the exhaustive verification (e.g., universe size 13). ↗

formal proof — A constant improvement is a short analytic proof checkable by referees or formalisable in Lean; an extended exhaustive verification is a re-runnable enumeration over union-closed families (with isomorphism reduction).

Progress: Gilmer's entropy method (Nov 2022) and follow-ups (Alweiss–Huang–Sellke, Chase–Lovett, Sawin, Pebody; Liu 2023; Lu–Raz 2024) pushed the constant just past 0.382; no proof of 1/2, and the (3-sqrt5)/2 barrier for the pure entropy approach is known.

status checked 2026-09-03 · sources: en.wikipedia.org, gilkalai.wordpress.com, semanticscholar.org

Statement: Place 2n points on an n x n grid with no three collinear. Constructions achieving 2n are known for all n up to the low 70s (with many recent additions), but the best general construction gives only (1.5 - o(1))n. Targets: a 2n-point configuration for the smallest n not yet achieved, or an algorithm producing > 1.8n points for arbitrarily large n (Epoch FrontierMath open-problem formulation). ↗

program checker — Check a point set for collinear triples in O(m^2) using gcd-normalised slopes; an asymptotic family requires a proof or a generator plus checks at many n.

Progress: Epoch AI (2026) reports 2n constructions verified for n <= 70, many found recently; July 2026 solved the analogous no-(k+1)-in-line problem for k > 2 (value kn), but the k = 2 case is untouched. Guy–Kelly conjecture that the asymptotic maximum is ~ (pi/sqrt3) n ~ 1.814n.

status checked 2026-09-03 · sources: epoch.ai, en.wikipedia.org, arxiv.org

Statement: Find the maximum over 10-point configurations in the unit square of the minimum triangle area, Delta_10, and certify it. Optimal configurations are now certified for n <= 9 (Delta_9 = -11/64 + 9 sqrt65/320); n = 10 is the smallest open case, with Comellas–Yebra's 2002 configuration the best known. ↗

program checker — A better configuration is verified by computing all C(10,3) triangle areas exactly; an optimality certificate is a branch-and-bound tree (MIP/interval arithmetic) that must be re-run or checked by a certificate checker.

Progress: Sudermann-Merx (arXiv Mar 2026, rev. May 2026) certified optimality for n = 5..9 in the unit square via mixed-integer optimisation with exact algebraic coordinates; a July 2026 paper certified n <= 8 in the unit triangle. n = 10 and 12 configurations remain best-known but unproven.

status checked 2026-09-03 · sources: arxiv.org, arxiv.org, en.wikipedia.org

Statement: Let M = lim M(n)/n where M(n) is the minimum over partitions of {1..2n} into two n-sets A, B of max_k |{(a,b): a - b = k}|. Known: 0.379005 <= M <= 0.380868. Target: an explicit step-function construction lowering the upper bound below 0.380868, or an improved lower bound. ↗

program checker — An upper-bound construction is a step function whose overlap integral is evaluated numerically with rigorous error bounds (public verifier code exists in the AlphaEvolve repository and EinsteinArena).

Progress: Published: Haugland 0.38093 (2016) -> AlphaEvolve 0.380924 (May 2025) -> TTT-Discover 0.380876 (2026) -> SimpleTES 0.380868 (2026). ARENA (EinsteinArena, agents' leaderboard) is ahead of publications: 0.3808586 (CodexProLong, L=3584). Sinapolis 2026-09-03: 0.380858574599 (polish of arena leader, +2.6e-10), submitted. Lower bound 0.379005 (White 2022).

status checked 2026-09-03 · sources: en.wikipedia.org, arxiv.org, einsteinarena.com, github.com

Statement: For every integer n > 1, 4/n = 1/x + 1/y + 1/z has a solution in positive integers. Verified for all n <= 10^18. Targets: extend certified verification (only primes in the 198 residue classes mod 120120 not covered by Mordell/Terzi need checking), or a proof. ↗

program checker — Verification runs produce, per residue class, a witness (x,y,z) or a modular identity; a checker recomputes 4/n = 1/x+1/y+1/z for sampled n and re-derives the covering identities.

Progress: Mihnea & Bogdan (arXiv Aug 2025) extended verification from 10^17 (Salez 2014) to 10^18; a Feb 2026 arXiv paper gives explicit parametric solutions for a density-one set; INTEGERS 26 (2026) paper on structure of solutions.

status checked 2026-09-03 · sources: erdosproblems.com, arxiv.org, arxiv.org

Statement: Determine the smallest N such that every N points in general position in the plane contain 7 in convex position. Known: ES(4)=5, ES(5)=9, ES(6)=17 (Szekeres–Peters 2006); conjecture ES(n) = 2^(n-2)+1 gives ES(7) = 33, and 33 <= ES(7) is known. Target: a SAT/enumeration proof that every 33 points contain a convex 7-gon. ↗

program checker — A SAT-based proof yields DRAT/LRAT proofs checkable by verified checkers (cake_lpr); a counterexample (33 points with no convex heptagon) is checked by enumerating 7-subsets (O(33^7) or via realisability of an order type).

Progress: Bogdan (Dec 2025) reports a triple-orientation SAT encoding with UNSAT certificates for anchored subfamilies of 33-point configurations, but the full case is computationally open; Heule–Scheucher's 2024 empty-hexagon SAT proof (30 points) is the methodological template. Erdős $500 / Graham $1000 prizes for the general conjecture.

status checked 2026-09-03 · sources: erdosproblems.com, en.wikipedia.org, arxiv.org

Statement: Determine W(2,7): the least N such that every 2-colouring of {1..N} contains a monochromatic 7-term arithmetic progression. Known exact values end at W(2,6) = 1132 (Kouril–Paul 2008); W(2,7) > 3703. Targets: a 2-colouring of {1..3704} with no monochromatic 7-AP (raising the lower bound), or a SAT proof of the exact value. ↗

program checker — A colouring is checked for 7-APs in O(N^2); an exact-value proof would be a huge SAT/DRAT certificate (W(2,6) took 253 CPU-days in 2008) requiring proof-checking infrastructure.

Progress: No exact value beyond W(2,6); lower bounds for W(2,7) and mixed cases (W(3,5) > 2173, W(4,4) > 1048) come from cyclic-zipper and distributed constructions (Rabung–Lotts 2012 and later). Conjecture (Kouril–Paul) that W(2,7) = 3704 is unproven.

status checked 2026-09-03 · sources: en.wikipedia.org, cs.umd.edu, combinatorialpress.com

Statement: Determine S(6): the largest n such that {1..n} can be 6-coloured with no monochromatic solution to x + y = z. Known S(5) = 160 (Heule 2017, 2 PB proof) and S(6) >= 536 (Fredricksen–Sweet 2000). Targets: a sum-free 6-colouring of {1..537}, or a SAT proof that S(6) = 536. ↗

program checker — A colouring is checked for x+y=z monochromatic triples in O(n^2); an upper-bound proof is a DRAT/LRAT certificate checked with a formally verified checker (as done for S(5)).

Progress: S(5) = 160 was settled by Heule (AAAI 2018) with a 2-petabyte DRAT proof; S(6) has no new bounds since 2000 in the sources consulted. Boolean Pythagorean triples (7825, Heule–Kullmann–Marek 2016) shows the SAT-proof paradigm at this scale.

status checked 2026-09-03 · sources: cdn.aaai.org, ar5iv.labs.arxiv.org, en.wikipedia.org

Statement: Does a rectangular box with integer edges a,b,c, integer face diagonals and integer space diagonal exist? Exhaustive searches show none with odd edge < 2.5e13, smallest edge < 5e11, or space diagonal < 9e15 (Matson 2015; Belogourov 2019/2020). Target: extend a certified search or find a cuboid. ↗

program checker — A candidate is verified by seven integer squarings; an extended search must publish code and per-range checksums for independent re-execution.

Progress: No perfect cuboid found; bounds as of 2020 stand. Several 2022-2025 arXiv/viXra 'non-existence proofs' (e.g., arXiv 2206.06160) are not accepted.

status checked 2026-09-03 · sources: en.wikipedia.org, mathworld.wolfram.com, unsolvedproblems.org

Statement: Show that 1^k + 2^k + ... + (m-1)^k = m^k has no solution other than 1 + 2 = 3 (k=1, m=3). Known: any further solution has m > 10^(10^9) (Gallot–Moree–Zudilin 2011) and k even. Target: raise the bound (continued-fraction method) or new congruence constraints. ↗

formal proof — Bound improvements rest on computing a continued fraction of log 2 / N to huge precision plus elementary congruences; both are re-computable, and the argument is short enough for referee checking or Lean formalisation.

Progress: Gallot–Moree–Zudilin bound m > 10^(10^9) (2011) is still the record; an Aug 2026 arXiv paper studies the equation over arithmetic progressions.

status checked 2026-09-03 · sources: en.wikipedia.org, arxiv.org, arxiv.org

Statement: Determine BB(6), the maximum number of steps a halting 6-state 2-symbol Turing machine takes from a blank tape (BB(5) = 47,176,870, proved 2024). Known: BB(6) > 2^^^5 (mxdys, June 2025). Concrete subtargets: decide holdout machines from the bbchallenge list (~1,100 as of Aug 2026), or resolve cryptids like Antihydra (Collatz-like). ↗

program checker — Halting proofs are certified by acceleration certificates or Coq/Lean deciders (as with BB(5)); non-halting proofs must be accepted by the bbchallenge decider pipeline; a new champion is verified by simulating (with acceleration) to the halting step.

Progress: Champion 1RB1RA_1RC1RZ_1LD0RF_1RA0LE_0LD1RC_1RA0RE gives BB(6) > 2^^^5 (June 2025). Wiki (updated 31 Aug 2026) lists ~1,101 informal holdouts, ~150 needing simulation to 1e14 steps; Antihydra (June 2024) and other cryptids make an exact value likely unreachable without solving Collatz-like problems. Monitor 2026-09-16: Reduced holdouts to 964 (2026-09-15). Monitor 2026-09-26: Added BMO8 and friend to cryptids list (2026-09-24). Monitor 2026-10-05: Holdout count updated on 2026-10-04

note: progress from source https://wiki.bbchallenge.org/wiki/BB(6) — verify

status checked 2026-09-03 · sources: wiki.bbchallenge.org, wiki.bbchallenge.org, quantamagazine.org

Statement: Extend the exhaustive verification that every even n >= 4 is a sum of two primes. Peer-reviewed frontier: 4e18 (Oliveira e Silva, Herzog, Pardi, Math. Comp. 2014). Target: a certified, independently reproducible extension (e.g., to 1e19) with published minimal-prime witnesses per interval. ↗

program checker — Re-run the segmented sieve with the published algorithm on the claimed intervals and compare the recorded minimal Goldbach partitions / checksums; sampling plus full recomputation of a fraction is standard.

Progress: April 2025: Hiroaki Jay Nakata's browser-based 'Gridbach' project announced verification to 4e18 + 7e13 (open-source, not peer-reviewed); a 2025 preprint also claims extension beyond 4e18. The 2014 result remains the accepted record.

note: source changed 2026-09-28: https://en.wikipedia.org/wiki/Goldbach%27s_conjecture

status checked 2026-09-03 · sources: medium.com, preprints.org, researchgate.net

Statement: Determine the minimum number of comparators in a sorting network on 17 channels. Best known: 71 comparators (depth 10, which is optimal); proven lower bound 63. Optimal sizes are known for n <= 12 (Codish et al. 2014) and depths for n <= 17. Target: a 17-input network with <= 70 comparators, or a proof that 71 is optimal. ↗

program checker — A network is verified by the 0-1 principle: simulate all 2^17 binary inputs (instant); optimality proofs are SAT-based with DRAT certificates and prefix/symmetry arguments that must be checked.

Progress: Dobbelaere's list (2026) records size 71 / depth 10 for n = 17 (SorterHunter), size 77 for n = 18, 85 for n = 19, 91 for n = 20, with size lower bounds 63/68/73/78; no size-optimality proof beyond n = 12 (Harder 2020-2021 verified n <= 12 with SAT).

status checked 2026-09-03 · sources: bertdobbelaere.github.io, jix.one, link.springer.com

Statement: Improve the best proven upper bound on the exponent omega of matrix multiplication (n x n product in O(n^omega)). Record: omega < 2.371177 (Aug 2026). Target: any strictly smaller bound with a verifiable laser-method / combination-loss analysis (these proofs reduce to checking finite optimisation certificates). ↗

formal proof — The bound follows from a finite set of parameters (distributions over tensor-power partitions) whose feasibility is checkable numerically with rational arithmetic; referees re-run the optimisation certificate scripts released with the paper.

Progress: 17 Aug 2026: Dupont, Eisenberger, ..., Alman, Vassilevska Williams, Balog (DeepMind + MIT) improved omega < 2.371339 (Alman–Duan–VW–Xu–Xu–Zhou 2024) to omega < 2.371177 using modern optimisation and AlphaEvolve on the combination-loss framework.

note: source changed 2026-10-07: https://arxiv.org/list/cs.DS/new

status checked 2026-09-03 · sources: arxiv.org, emergentmind.com, arxiv.org

Statement: Does a 57-regular graph on 3250 vertices with girth 5 (diameter 2) exist? Hoffman–Singleton (1960) showed such Moore graphs can only have degree 2, 3, 7 or 57; the first three exist and are unique. Target: construct the graph, or prove non-existence. ↗

program checker — Given an adjacency list (3250 vertices, 92,625 edges), check 57-regularity and that every pair of non-adjacent vertices has exactly one common neighbour and adjacent pairs none (O(n^2 * d)); non-existence would need a proof.

Progress: Ishida (arXiv June 2026) proved the graph, if it exists, has no involutory automorphisms, so its automorphism group has odd order (strengthening Mačaj–Širáň's |Aut| <= 375 and earlier results). Faber–Keegan (2022) reviewed why existence remains open.

status checked 2026-09-03 · sources: arxiv.org, arxiv.org, mdpi.com

Statement: Does a strongly regular graph srg(99, 14, 1, 2) exist: 99 vertices, each of degree 14, every edge in exactly one triangle, every non-adjacent pair with exactly two common neighbours? Conway offered $1,000. A solution is a list of 693 edges. ↗

program checker — Check the 99x99 adjacency matrix A satisfies A^2 + A - 12 I = 2 J (integer arithmetic, milliseconds); non-existence would need a certified exhaustive search (DRAT) over automorphism-group cases.

Progress: April 2026 arXiv: SAT-solver approach with symmetry breaking (no graph found, structural exclusions); Aug 2026 arXiv: forced-structure reduction with verifiable bounds. Existence remains open; Epoch AI lists it as a FrontierMath open problem.

status checked 2026-09-03 · sources: epoch.ai, arxiv.org, arxiv.org

Statement: A Sudoku puzzle is minimal if it has a unique solution and removing any clue destroys uniqueness. The minimum clue count is 17 (McGuire–Tugemann–Civario 2012, no 16-clue). The maximum is open: the largest known minimal puzzle has 40 clues. Target: a 41-clue minimal Sudoku, or a proof that 40 is the maximum. ↗

program checker — Run a solver to confirm uniqueness, then confirm that each of the 41 single-clue removals yields >= 2 solutions (42 solver calls, milliseconds).

Progress: 40-clue minimal puzzles are known (community 'snipes' records, sudokutheory.com); no 41-clue example and no upper-bound proof as of the sources consulted.

note: source changed 2026-10-06: https://en.wikipedia.org/wiki/Mathematics_of_Sudoku

status checked 2026-09-03 · sources: en.wikipedia.org, sudokutheory.com, arxiv.org

Statement: The chromatic number of the plane is 5, 6 or 7 (de Grey 2018 proved >= 5 with a 1581-vertex unit-distance graph; Polymath16 reduced this to 509 vertices by 2021). Concrete targets: a 5-chromatic unit-distance graph with fewer than 509 vertices (SAT-checkable), or a 6-chromatic one (would raise the lower bound to 6). ↗

program checker — Verify all listed edges have exact unit length (algebraic coordinates, exact arithmetic) and that the graph has no proper 4-colouring via a SAT solver with a DRAT proof (seconds to minutes).

Progress: Aug 2026 arXiv: a Moser-spindle-free 5-chromatic unit-distance graph on 2131 vertices (structural, not a size record). Smallest known 5-chromatic graph remains 509 vertices (Parts, 2021 per Wikipedia); no 6-chromatic graph known.

note: source changed 2026-10-07: https://en.wikipedia.org/wiki/Hadwiger%E2%80%93Nelson_problem

status checked 2026-09-03 · sources: en.wikipedia.org, arxiv.org, michaelnielsen.org