Records
Results with a machine-checked certificate. Each entry gives the exact claim, what was known before and how to check it. Where stated, it also gives the hash of a manifest of the certificate with an OpenTimestamps proof that anchors that hash in a Bitcoin block.
Condorcet winning sets
Three candidates suffice for elections with 7 or 8 candidates
Last updated 2026-10-14
29 September 2026 · Recomputed by a second agent on a different model provider, directed by the same author, and checked by a formally verified proof checker · Not peer reviewed
Each of n voters ranks m candidates. A set W of candidates is a Condorcet winning set if, for every candidate c outside W, fewer than n/2 voters rank c above every member of W. A tie at exactly n/2 counts against W. This is the definition of Elkind, Lang and Saffidine (2015) and of Charikar et al. (2025), who conjecture that size 3 always suffices.
Every election with m = 8 candidates and any number of voters has a Condorcet winning set of size 3. The same holds for m = 7. A counterexample to the conjecture therefore needs at least 9 candidates.
Version 2 of Zilberstein, Martins and Berker (10 October 2026) reports the same conclusion for every election with at most 8 candidates, from Gurobi mixed-integer programming with numerical tolerance 10−6. What this record adds is an exact, formally checked proof for 7 and 8 candidates, whose certificates were timestamped on 29 September 2026. The two methods share no code.
Limits
- Not peer reviewed. The evidence is the checker output, which anyone can reproduce.
- The step from the theorem to the SAT formula is about 150 lines of Python. It was written twice, independently, and both versions produce the same formulas. It is not formally verified, and there is no Lean statement. The formal guarantee stops at “the parsed formulas are unsatisfiable”.
- For m = 8 the second agent reran the same 21 proof files with the same cake_lpr binary: one proof checked twice, not two independent proofs.
- This settles two finite cases. It does not settle any case with 9 or more candidates, and it does not improve the general bound of 5 to 4.
Check it
The public repository Aspect5/condorcet-certificates holds the generators, the certificates and verify.sh. The proofs are attached to its release. One command regenerates every formula, downloads and hash-checks the proofs, and runs cake_lpr on all 22 (about 20 minutes of wall time on the measured host with a 32 GiB memory cap; the full run at the pinned verifier commit 7e68ba6 took 23 min 2 s, and earlier full runs took 17 min 47 s and 22 min 18 s). DOI pending.
Preprint: Condorcet winning sets of size three for elections with seven or eight candidates (10 pp., revised 14 October 2026, PDF, SHA-256 fb84ed653f4042e96693a51dddc56113d73927fe0a5a5dec57978e999ddf31c7). Not peer reviewed. It also proves the exact bounds α*(7,3) ≤ 2/5 and α*(8,3) ≤ 9/19; version 2 of Zilberstein, Martins and Berker reports floating-point upper values 0.400 and 0.444 for these.
Manifest and timestamp
Manifest SHA-256: ae319c72fe646532c836856be0f86572b8c92d10b84c6de9050815d572c77555. The manifest lists every file of the certificate, including all formulas and proofs. Its OpenTimestamps file anchors the manifest’s hash in Bitcoin block 969212 (2026-09-29 22:18 UTC), which proves the manifest existed by that block’s time; matching hashes tie the formulas and proofs to that manifest. Check it with ots verify MANIFEST.sha256.ots. A first manifest (OpenTimestamps file, anchored in Bitcoin block 969208, 2026-09-29 21:42 UTC) has the same proof hashes; it predates edits to three documentation files.
What was known
For even n at 7 and 8 candidates, Elkind et al. give size 4. The general bound is 5 (Song, Nguyen and Lin, 2025).
Method
If some election had no winning set of size 3, every 3-set would have a challenger ranked above all of it by at least half the voters. We encode the choice of challengers as a SAT formula. Its clauses come from exact rational certificates, each showing that a small set of challenge events cannot all hold at once, checked over all 40,320 rankings of 8 candidates, together with all their relabelings. For m = 8 the formula has 4,161,137 clauses. It is split into 21 cases, each refuted by the CaDiCaL solver with an LRAT proof (5.05 GB compressed), and every proof is verified by cake_lpr, a proof checker whose correctness is itself formally proved. The m = 8 argument uses no earlier result. The m = 7 case needs one proof of 55 MB compressed.
How it was made
AI agents at IRSI, using Anthropic Claude and OpenAI Codex models, found, built and checked the certificates, directed by Peter Seelman. For m = 8, one agent built the certificate and an agent using the other provider's models recomputed it with its own generator. For m = 7, three separate agents built, recomputed and proof-checked it.
The pentagonal bipyramid minimizes logarithmic energy for 7 points
1 October 2026; 2 October 2026 (cross-provider check) · Computer-assisted proof · Every piece rechecked by separate agents. On 2 October 2026 an OpenAI GPT-6 agent independently re-derived the local analysis, the outer-region replay (413,407 leaves, 0 failures) and the seam, and accepted them. The 65.8-million-leaf global cover has not been replayed by another provider · Not peer reviewed · Not formalized in Lean
Among all configurations of 7 distinct points on the unit sphere in R3, the logarithmic energy ∑i<j −log|xi − xj| is minimized exactly by the pentagonal bipyramid (a regular pentagon on the equator and the two poles), with energy −(6 log 2 + (5/2) log 5), and only by its images under orthogonal maps and relabeling.
What was known
An independent proof by a different method was posted first: an AI-produced Lean 4 formalisation with three-point semidefinite certificates (alejandrozarco/thomson-n7-log, Zenodo; certificates 29 September 2026, Lean 1 October 2026; not peer reviewed). Ours was found separately; our agents first saw that repository on 1 October 2026, after our proof was posted. Armentano et al. (arXiv 2502.10152) showed the bipyramid is the only critical configuration containing an antipodal pair. The same configuration is the proved minimizer of Coulomb energy for 7 points (Vals AI, Lean 4, not peer reviewed), and Kryvonos, Liehr and Taylor proved the 8-point case for logarithmic and Coulomb energy (arXiv 2609.22077). Melnyk, Knop and Smith (1977) studied power-law energies with exponent at least 1, numerically and without proof, and did not treat logarithmic energy.
How it is proved
Three pieces. Configurations in which no two points are nearly antipodal (smallest pairwise inner product m ≥ −97/100) are excluded by a positive-semidefinite certificate built on Bachoc–Vallentin kernel positivity, with certified energy margin at least 7.7 × 10−5. The rest of the space is covered by 65.8 million boxes in 378 charts, each checked in outward-rounded interval arithmetic; the 234,361 thinnest boxes were rechecked at 256-bit precision (smallest certified energy margin 6.4 × 10−23, in units of the energy). Near the bipyramid, where the Hessian is degenerate, a quartic local analysis finishes the proof. The logic of the case split that joins the pieces is checked in Lean 4, with the three pieces taken as hypotheses.
Limits
- Claude agents built and rechecked the global cover. A replay by another provider has not been run.
- The local analysis (L7-A2, L8, L9) is checked across providers. On 2 October 2026 an OpenAI GPT-6 agent accepted all three, including the steps of the L8 slice lemma that only Claude agents had checked before. It took the exact Hessian and coupling data as given; a GPT-6 agent derived those and a Claude agent recomputed them exactly.
- The written lemmas are paper proofs checked by agents, not by a human expert.
- A preprint and the certificate (about 43 MB) will be posted after the cross-provider check.
The 3-sunflower-free capacity is at least 1.5647730
Last updated 2026-10-17
17 October 2026 (earlier values 1.5617847 on 30 September and 1.5621220 on 1 October 2026) · Exact certificate, accepted by three exact checkers written separately. One was written from scratch by OpenAI GPT-6.1 Sol (a second model provider), given only the definitions and the 1997 paper: it checked all 20,100,970 containment pairs and 292,854,591 sunflower completions, re-derived the transfer matrix and the gluing lemma, isolated the root with exact rational arithmetic, and rejected a planted sunflower, a planted containment and an inflated bound · Not peer reviewed
A family of subsets of an n-element set with no three members whose pairwise intersections are all equal has at most μ3n+o(n) members. Gluing copies of a 6,341-set Sperner, 3-sunflower-free family on 20 points (the chain construction of Lemma 4.4 of Deuber, Erdős, Gunderson, Kostochka and Meyer, 1997) gives μ3 ≥ ((3901 + √5882425)/2)1/18 = 1.5647730960…, against 1.551 in that paper and an unpublished 1.554.
Check it
Aspect5/sunflower-free-capacity, tag v1.2: certificate cert_c49_chain20_v12.json (SHA-256 7472112ced9d98da8cf7b6a3d586b93ea66750e39989e7a6d6d5f52ffeb4e82e). Run python3 check_openai_v12.py in that folder (standard library only, about 15 seconds; exits 0 on ACCEPT). The other two checkers: python3 check_c49.py cert_c49_chain20_v12.json --claim 1.564773096 and python3 recheck_c49.py cert_c49_chain20_v12.json, which scans all triples.
Consequences and earlier values
The 1.5621220 chain also gives the Erdős problem #856 constant γ3 ≥ 0.4458 by Corollary 1.2 of arXiv 2609.07268 (published: 0.4389). That step was independently recomputed on 2 October 2026 by an OpenAI GPT-6 agent, which re-derived the transfer matrix and rejected three planted wrong variants. With a weighted version of the same chain (z = 5733/5000, the paper’s Theorem 4.1) the bound improves to γ3 ≥ 0.4496442592. That value was also recomputed independently by the GPT-6 agent. A separate scan of public sources on 2 October 2026 found no matching or higher value. The scan covered arXiv, Semantic Scholar, Tao’s problem list, GitHub and Zenodo; the erdosproblems.com comment thread for #856 could not be read (HTTP 403), so this compares with the published bound only. The current value is in a pull request to Tao’s optimization-problems list (entry 49a), with all three certificate versions in Aspect5/sunflower-free-capacity. Earlier values: 1.5617847 (30 September 2026) and 1.5621220 (1 October 2026), whose certificates are in irsi-certificates-2026-10-01.zip (SHA-256 f89d9255e75860d4a9d08ab2b96ac8b891a02bf53340171c9320563a2afe3a6d, folder sunflower) with three exact checkers, one by Google Gemini, and an OpenAI GPT-6 recheck.
Larger grid sets with no four points on a circle or line: n = 19, 23, 24, 25, 26, 27, 30
1 October 2026 (n = 24, 27, 30); 2 October 2026 (n = 19, 23, 25, 26) · Exact certificates (integer arithmetic), each accepted by three exact checkers written separately, one of them by Google Gemini (a second model provider) · Not peer reviewed
The largest set of points of the n × n grid with no four on a common circle or line has at least 37 points for n = 19, 45 for n = 23, 46 for n = 24, 48 for n = 25, 50 for n = 26, 51 for n = 27 and 56 for n = 30. AlphaEvolve’s lower bounds (arXiv 2607.05255, July 2026) are 36, 44, 45, 47, 49, 50 and 55. We match its values for n = 15, 17, 20, 21, 22, 28 and 29 and fall short for n = 14, 16 and 18. All three sets are centrally symmetric and were found by tabu search.
Check it
irsi-certificates-2026-10-01.zip (523 KB, SHA-256 f89d9255e75860d4a9d08ab2b96ac8b891a02bf53340171c9320563a2afe3a6d), folder no-four-on-a-circle: python3 check.py circ_n30_k56.json. The n = 19, 23, 25 sets: irsi-certificates-2026-10-02.zip (3 KB, SHA-256 e65a5d4f7ced9fe5d2f8797dd6646137543180206f864537559b3eb3315de6ce; OpenTimestamps proof). Second checker, written separately (standard library; tests every 4-subset with the determinant det[x, y, x²+y², 1]): recheck_circ.py, run as python3 recheck_circ.py circ_n30_k56.json 56. The n = 26 set: irsi-certificates-2026-10-02b.zip (SHA-256 a414a5a66360d78120de71d0f5cfd3cf0b94e86af76bb5ca2019b25fbb0ca891; OpenTimestamps proof).
Strength-3 covering arrays
One construction improves 12 covering-array bounds CAN(3, q+2, v)
1 October 2026; 2 October 2026 (third checker) · Every array accepted by three exact checkers written separately, one of them by Google Gemini (a second model provider), which checks every column triple exhaustively. On 3 October 2026 an OpenAI GPT-6 agent (a third provider) rechecked all 12 arrays with its own exact checker, rejected planted faulty arrays, and audited the construction’s coverage proof line by line · Not peer reviewed
A recursive construction gives, for odd prime powers q, CAN(3, q+2, q) ≤ q3 + q(q2−1)/2, against 2q3 − q2 − q from Lemma 3.3 of Colbourn, Kéri, Rivas Soriano and Schlage-Puchta (2010). It improves the November 2024 state of Colbourn’s tables in 12 cells (v = 8 to 19). Seven of them were listed in Tables on 25 September 2026 (for v = 10 and 12 a search refinement gives the smaller values shown there). New today: CAN(3,11,8) ≤ 852 (was 960), CAN(3,11,9) ≤ 1,089 (was 1,175), CAN(3,21,18) ≤ 9,902 (was 11,500), CAN(3,21,19) ≤ 10,279 (was 11,791) and, by only 8 rows, CAN(3,21,17) ≤ 9,529 (was 9,537). A preprint is in preparation.
Check it
irsi-certificates-2026-10-01.zip (523 KB, SHA-256 f89d9255e75860d4a9d08ab2b96ac8b891a02bf53340171c9320563a2afe3a6d), folder covering-arrays: python3 check_ca.py CA_N852_t3_k11_v8.txt --t 3 --k 11 --v 8 --n 852. Independent checker: verify_ca_gemini.py (standard library), run with the same arguments.
Later search results
Later computer search found smaller arrays for seven cells, all on the Tables page and accepted by an exhaustive checker written by Google Gemini. They include CAN(3,11,8) ≤ 834, CAN(3,21,17) ≤ 9,038 and CAN(3,21,18) ≤ 9,524. Three of the seven came from a control run with no language model in the loop, and that control matched or beat the lab’s model-guided search on 4 of 5 cells.
Fault-tolerant sparse state preparation with about 0.43 Toffolis per amplitude at s = 4,096, with few clean qubits
2 October 2026 · Checked by the builder (exact Toffoli recount, 200 sparse simulations to fidelity 1 − 2.2 × 10−15, planted faulty circuits rejected) and by an independent simulator written by Google Gemini from the published format alone (Toffoli count 1,776, fidelity 1 − 2.4 × 10−15, ancillas returned to |0⟩, borrowed qubits restored) · Not peer reviewed
Preparing an n-qubit state with s nonzero amplitudes (n = 32, random supports) takes 1,776 Toffoli gates at s = 212 with 39 clean qubits plus borrowed (dirty) qubits that are returned unchanged, against 8,463 Toffolis and 43 clean qubits in the worst-case construction of arXiv 2601.09388 (Table 1). The ratio grows from 1.8 at s = 29 to 22.9 at s = 216; at s = 28 ours is worse than their random-state figure. The construction (dense labels, then dirty-qubit QROM copies and a displacement-table relabel with no slack) follows the framework of arXiv 2607.28260; new here are the dirty-qubit use, the zero-slack relabel with a proof that one random draw succeeds with probability above 3/8 when n ≥ 2m + 2, explicit constants and emitted, checked circuits. The 0.43s figure is measured on 8 supports, not proved for all.
Scope: this is not a new asymptotic result. Li et al., arXiv 2607.28260 (Theorem 4.2, p. 24), already prepare s-sparse states with a T count sublinear in s, better than our O(√(sn)). They use about √(sn) clean ancillas, and the sublinear question is marked answered in v2 of 2601.09388. What is ours: the regime of n + m − 1 clean qubits plus borrowed idle qubits, explicit constants, and emitted, checked circuits. The comparison above is against 2601.09388 at that clean-qubit count, not against the best published method. We have not yet costed the most direct competing route (a dirty-qubit lookup inside 2607.28260), so the size of our advantage there is unknown. No preprint until that is done.
Central circle constant
Upper bound on the central-circle constant C* lowered from 0.141913 to 0.140871
2 October 2026 · Exact certificate, accepted by two exact checkers written separately: one by a Claude agent (square roots rounded up at 2−80) and one by Google Gemini (a second model provider) from the theorem statement alone. On 3 October 2026 an OpenAI GPT-6 agent (a third provider) rechecked the certificate with exact arithmetic and obtained 0.14087056029839208, below the stated 0.14087056030 · Not peer reviewed
Place n nonoverlapping circles of radii 1, 2, …, n around a central circle, each touching it from outside. The least possible central radius is C* n2 + o(n2) (Falconi, arXiv 2609.13630, September 2026), and that paper proves 0.14056946887 < C* ≤ 0.14191330339. We show C* ≤ 0.14087056030, which cuts the width of the known interval by 77.6% (from 1.34 × 10−3 to 3.01 × 10−4). The certificate is an explicit order of n = 480,000 circles. The paper’s Theorem 4 turns any such order into an upper bound on C*. A linear program over alternating orders found the order, and its continuum value is 0.1408619. The lower endpoint is unchanged.
Check it
irsi-central-circle-2026-10-02.zip (456 KB, SHA-256 3db7a4eb355eeb54654a9d790825087122111ee29544d7c27ab165c24ad5ad32; OpenTimestamps proof). Run python3 verify_upper.py word_n480000.txt.gz 0.14087057 to get ACCEPT. The independent checker python3 verify_cc_gemini.py word_n480000.txt.gz rounds more coarsely and prints 0.140870813966.
qLDPC code
A weight-6 two-block code [[124,2,16]]
30 September 2026 · Distance by two exact methods and a recomputation by a second agent on a different model provider, directed by the same author · Not peer reviewed · Not in the catalogues checked on 30 September 2026
Let l = 62, a(z) = 1 + z and b(z) = 1 + z36 + z47 + z54 in F2[z]/(z62 − 1), and let A and B be their 62 × 62 circulant matrices. The CSS code with HX = [A | B] and HZ = [BT | AT] has n = 124 qubits, k = 2 logical qubits and minimum distance dX = dZ = 16. Every check acts on 6 qubits, and every qubit is in 2 or 4 checks of each type.
Check it
Download qldpc-124-2-16-2026-09-30.zip (SHA-256 6060fe41c89f0a78886de24d67d7a21117e4b0a884389b1ff09ebd22c3418a0c). python3 check_qldpc_124_2_16.py (standard library only) checks commutation, k = 2, the check weights, and two weight-16 logical operators, so d ≤ 16. gcc -O3 -o bz bz.c, then ./bz 62 X "0 1" "0 36 47 54" and the same with Z, runs the exhaustive search that gives d ≥ 16. The zip also holds the solver summary of the independent integer program.
What was known
Catalogue distances are listed values; the Challenge board and the Wang–Pryadko and Lin–Pryadko searches report upper bounds, not exact distance certificates.
At weight 6 this saves 4 qubits over [[128,2,16]]. It is a small catalogue improvement, not a new construction: Lin and Pryadko’s fit for this family, d ≈ −1.840 + 1.572√n, gives 15.7 at n = 124, so the code sits on the known scaling curve. Codes with larger check weight already do better.
Method
A Brouwer–Zimmermann exhaustive search finds d = 16 in each sector in about 7 seconds. An exact integer program (HiGHS, gap 0) over the 3 nonzero logical classes, with cyclic symmetry broken into two branches, gives the same value, and 20 randomized QDistRnd runs never found a logical operator lighter than 16. An agent running OpenAI’s GPT-6.1 Sol then rebuilt the code and wrote its own integer program; all 12 of its branches for this code closed (8 optimal, 4 infeasible), giving dX = dZ = 16, and a separate checker confirmed every optimal support. A [[116,2,15]] code from the same search is already on qecdb and the Challenge board, so it is not claimed here.
Limits
- Neither program is formally verified, and the integer program’s output is a solver log, not a proof certificate. There is no Lean statement.
- Only the four sources above were searched. The code may exist elsewhere, and a weight-8 code in these catalogues might have another generating set of weight 6; that was not checked.
- Not submitted to either catalogue.
How it was made
An AI agent found the polynomial pair in a computer search. A second agent rebuilt the code and computed its distance, and a third, using the other provider’s models, recomputed it with its own code.