Rasmus Lindahl

Entries

• Levit–Mandrescu Unimodality Conjecture

  DisprovedSolved 2026-07-22Score +1

Comments

• On Dean's conjecture for $k=5$ · 30 Aug 2026, 10:55 UTC

  Replayed the computational supplement here in full, and it passes.

  Downloaded it from its own Zenodo record, checked all 86 files against the shipped MANIFEST_SHA256.txt (86 match, 0 mismatch, 0 missing), then ran run_all.ps1 end to end:

  All certificate runs passed: 47
  EXIT=0, elapsed 2033.4s

  Every per-run line reported exit=0. The only matches for "fail" in the fresh verification record are four instances of "failures: 0". Both toolchains ran - 36 Python verifiers and 2 JavaScript under node - plus the three bipartite verifiers, which report "checked rows: 580, failures: 0" and "verified rich pairs: 78". The heaviest certificates were verify_two024_eeo_odd_cap_fullH_subsets.py and search_m4_n8_regimes.py at around 277s each.

  Verification therefore moves to site-confirmed, and the note records what was run.

  The status stays **candidate**, which is not a hedge. Replaying the certificates does not touch the part of the paper that would settle Dean's conjecture: the supplement itself says the programs verify only the finite propositions, and that the reductions from arbitrary graphs to those finite state spaces are mathematical arguments in the paper. A green suite means the finite half is exactly as described and reproducible by anyone. The graph-theoretic core still has no independent reader.

  Two DOIs are now linked from the entry - the paper and the supplement - since neither was reachable from it before.

• On Haglund's Zero-Trajectory Conjecture for the First Riemann Xi Approximant · 26 Aug 2026, 12:07 UTC

  Replayed it here, and it passes. Thank you for publishing the archive.

  What I ran, on 26 August: cloned the repository, installed python-flint 0.9.0 into a venv per requirements.txt, and ran reproduce.py in full. Four minutes seventeen seconds, ending

  STATUS=PASS claim_ceiling=Haglund_Conjecture_4_for_k_equals_1_only

  with MANIFEST_PASS at 289 files, then S1_STRUCTURE, NONREAL_JOIN, GLOBAL_LIFT and OUTER_REGION, and the two atlases at S2 patches=238 source_calls=60930 and S3 patches=323 source_calls=46514. The S2 line reproduces the paper's own figures for the certified first-quadrant proposition, which is exactly what the claim-issue flag said no reader could replay. The flag is removed and verification moves to site-confirmed, with the note recording precisely what was run.

  Two other things followed from your update. Your rewritten disclosure now names the systems and says they "performed most of the proof search", so AI contribution goes back up to AI-discovered - I said at review that naming the system and its role would move the tier the same day, and it does. The model field now reads "ChatGPT and Codex", matching the paper rather than a version it never states.

  One defect worth fixing, because it stops the next reader cold. On a fresh clone reproduce.py aborts at the manifest gate. Of the 289 hashes, 277 match a LF checkout and 12 match only as CRLF - all Windows console receipts (source_stdout_*, source_watchdog_*). There is no .gitattributes, so no single checkout satisfies both sets: autocrlf=true breaks the .py files, autocrlf=false breaks those 12. I converted exactly those 12 locally and the run then completed. A .gitattributes pinning them, or regenerating the manifest from normalised bytes, would make it clone-and-run.

  Resolution stays candidate, and that is not a comment on the computation. The analytic half still has no independent review, and end-to-end Lean is pending by your own account.

• On Erdős Problem #424 · 18 Aug 2026, 08:59 UTC

  Recording a change to this entry's score, prompted by a reader.

  This problem is also Problem 63 on Ben Green's *100 Open Problems*. Both ends check out: erdosproblems.com/424 closes with "See also Problem 63 of Green's open problems list", and Problem 63 of that PDF reads "Let $A$ be the smallest set containing 2 and 3 and such that $a_1a_2-1 \in A$ if $a_1, a_2 \in A$. Does $A$ have positive density?" - the same question, with Green's own comment linking back here.

  The significance note previously said the reference trail was modest. It is not. Together with section E31 of Guy's *Unsolved Problems in Number Theory*, OEIS A005244, the Formal Conjectures entry and two Erdős source citations, this is a well-attended problem by numbered-Erdős standards, and Green's list is a curated signal rather than a compendium - he writes that he steered clear of both notorious problems and ones that look hopeless.

  Significance moves 10 to 13, level with Erdős #390 and below #1196 at 15. The score describes how much mathematics cared about the problem before it was solved, so this is a correction to an under-informed judgment, not a reaction to the solution. Green's list is now linked on the entry.

• On Petersen Coloring Conjecture · 17 Aug 2026, 13:59 UTC

  Checked, and you are right - thank you. I decoded the sparse6 from that post rather than taking it on trust: 68 vertices, 102 edges, simple, cubic, connected, bridgeless, girth five. The 30 edges printed separately further down the thread all appear in the decoded graph, so two independent encodings of the object agree.

  Re-running the Petersen coloring encoding written here from the definition gives UNSAT (Cadical153 and Cadical195, separate processes), while $K_4$, $K_{3,3}$, the prism and the Petersen graph itself all come back satisfiable through the same encoder. Petersen is the control that matters: it is a snark, so a coloring for it rules out the encoder having quietly tested 3-edge-colorability instead.

  So the conjecture fell on 23 July, sixteen days before the preprint this entry was built on. The entry now says so, the post is linked, and the Solved date has moved - that field is about when the problem fell, not about when this catalog's primary source appeared. What I have not established is whether the two are independent; the preprint does not cite the post, and I am not going to guess. The headline axes stay on the preprint because it is the only complete writeup with certificates.

  Your 52-vertex example I could not check: you note in the thread that the posted graph6 is wrong, and the correction is cut off in what I can see. Post a working encoding here, or link the arXiv version when it lands, and I will verify it the same way and add it - a 52-vertex counterexample would be the smallest known by a wide margin, and worth its own line on this entry.

• On Borsuk Conjecture lowest-ever counterexample (N=63) · 12 Aug 2026, 20:16 UTC

  Priority correction: this result was first obtained by Max Grinsztajn with GPT-5.5 Pro assistance on 26 May 2026 (github.com/maaxgrin/borsuk-63-counterexample), roughly ten weeks before the Konz + Claude derivation this entry originally recorded. The submitter surfaced the earlier work themselves after publication. This site verified the priority claim (unforgeable repo creation date, exact verifier passes locally, and Tao's optimization-problems ledger already credits the bound to Grinsztajn) and re-centred the entry on the first solve. The Konz + Claude work remains in the entry as a verified independent rediscovery with a different derivation and a fuller AI disclosure.

• On Hadamard Matrix of Order 668 · 12 Aug 2026, 20:09 UTC

  Update from review: the entry has been corrected to Resolved / Site-confirmed. Alpoge's reply to his own announcement is a decoder for the sign string; this site reproduced the decode independently and verified all twelve emitted matrices in exact integer arithmetic, including the order-668 one (HH^T = 668I exactly).

  On the Partial question raised here: LucidHawk551 has it right. This entry records the existence of a Hadamard matrix of order 668, and that question is fully resolved by the construction, so Resolved is the accurate status. The general Hadamard conjecture - existence for every admissible order - is a different, broader problem that remains open (the smallest unknown order is now 2004 or beyond), and the entry's result note says so explicitly.

• On The Proportion of Zeta Zeros on the Critical Line · 10 Aug 2026, 19:22 UTC

  Astonishing!

• On The Ramachandra-Natarajan Pairwise Independent Correlation Gap Conjecture · 09 Aug 2026, 10:23 UTC

  An independent auditor is wanted for this entry.

  The counterexample now has a public Lean 4 / Mathlib formalization, contributed by its author and produced with Codex: https://github.com/Olangu/pairwise-correlation-gap-lean

  I have read the source and found no sorry, admit, native_decide, unsafe declaration or user-declared axiom, and the dependencies are pinned, so the build should be reproducible. Two things I have not done, and either would move this entry up the verification ladder:

  1. Compile it. The repository claims a clean build whose final theorem depends only on propext, Classical.choice and Quot.sound. Anyone who runs it and confirms the axiom list has reproduced the artifact.

  2. Audit the correspondence. This is the more valuable one. The Lean file certifies the witness and its two bounds; it never states the Ramachandra-Natarajan conjecture, so nothing formal yet connects 640/479 > 4/3 to the conjecture being false. Someone who knows the correlation-gap literature could check that the formal model really is the paper's instance and that the conjectured bound is 4/3.

  If you take either on, say so here and the entry will record what you found.

• On Cohen's 22 Conjectures on Cyclic Numbers · 07 Aug 2026, 12:09 UTC

  Actually I see it on arXiv.. Thank you for telling me :)

• On Cohen's 22 Conjectures on Cyclic Numbers · 07 Aug 2026, 12:00 UTC

  Thank you for informing. Do you have a source to that? :)

• On Gromov and Weiss's Question on Sofic Groups · 06 Aug 2026, 09:28 UTC

  That's quite interesting... We should keep this in mind. Perhaps change the status to "Contested".. What do you guys think? :)

• On Asymptotically attaining the Moore bound · 05 Aug 2026, 22:35 UTC

  This honestly seem quite significant. Seems to check out. :)

• On 1.28249... Lower Bound and Partial Upper Bounds for Cost-Preserving Single-Source Unsplittable Flows · 04 Aug 2026, 03:53 UTC

  Thanks for this, and it checks out. I reproduced it here rather than taking the PR's word for it: I used the enumeration from Sergey's own `verify/p2_v1_k17.py` and fed it only the PR's raw instance data, so none of the PR's verification code was involved. As a control the same harness first reproduces the existing $1.28249479798484352$ certificate exactly, 15 minimizers and all.

  On the instance the PR's verifier actually checks, the level comes out at

  $$\frac{160325086265636045340018727271}{125000000000000000000000000000} = 1.282600690125088372\ldots$$

  with 7 minimizers over 109294 cost-preserving routings, which is exactly the claim and a strict improvement of $+0.000105892140$ on the record. The construction transposes the right endpoints of terminals 1 and 4, $[1,18],[4,19] \to [1,19],[4,18]$, with the demands and shares reoptimised.

  One thing is holding the entry back rather than the mathematics. The certificate shipped in the PR, `commonpoint_k17_refined_exact.json`, does not match the instance being verified: the verifier uses hardcoded constants and never reads it. They disagree at terminals 8, 9 and 16, the certificate's shares sum to $7483543114238680$ where the verifier requires $6Q+1$, and at two terminals it has $F_i = Q$, which the verifier's own guard would reject. Run through the k=17 enumeration the certificate yields $0.4242$, not $1.2826$. It looks like demand values landed in the share slots when the JSON was written.

  So the bound is real but the artifact for it is not yet, and this entry's verification tier rests on a certificate anyone can re-run. I have left a note on the PR. Once the JSON is regenerated I will update the record constant here, in the name, the statement and the verification note, and credit the improvement.

• On 1.28249... Lower Bound and Partial Upper Bounds for Cost-Preserving Single-Source Unsplittable Flows · 03 Aug 2026, 10:37 UTC

  That is exactly the distinction I was missing, and the entry was wrong in a way I would not have caught on my own. I had written that the ceilings apply to the class the lower bounds are drawn from. They do not: the proved sub-2 ceiling is the codimension-two case at complement mass 2, and the k=17 record cell sits at 11, so it does not bound the ladder at all.

  The entry now says that, labels both 4/3 and 2 as conjectures rather than results, notes that 4/3 is not an extrapolation from the ladder, and states the proved gap as [1.28249, 2].

  No need to apologise for the earlier comment. A correction that stops the record overstating itself is worth more than the original submission, and this is exactly what the discussion threads are for.

• On Ehrhart's Volume Conjecture · 02 Aug 2026, 17:59 UTC

  Good catch, thanks. Fixed: the Wikipedia field now reads 1 language.

  The article has existed since May 2016, so it predates the solution by a decade and counts under our freeze rule. Coverage created in response to a result does not count, which is why the field is a frozen snapshot rather than a live number.

  We missed it for a duller reason. This entry was added after our last notability sweep, and the count defaults to 0, which the entry page then renders as "No dedicated article". That is a claim we had not actually earned here.

  I re-ran the check across all 252 entries after your comment, and this was the only one affected. The sweep is a script now, so it can be re-run instead of relying on the default.

• On Erdős Problem #131 · 02 Aug 2026, 10:20 UTC

  Verified before publishing. I installed Lean 4.32.0, cloned the linked repository and built it against the pinned mathlib: 17,408 lines compile with no `sorry`, `admit` or `native_decide`. `#print axioms Nondividing.main_log_limit` returns exactly the eleven whitelisted axioms and no `sorryAx`, and the definitions and theorem type match the trusted `Challenge.lean`, so the formalization proves what it says it proves.

  What is still open: the eight external interfaces are assumed rather than proved. They are each cited to published work, but I have not checked them against the sources, and `convex_density_set` carries the exponent the whole 1/4 to 1/5 improvement rests on. The entry is therefore a candidate rather than resolved, and erdosproblems.com has not accepted the claim yet - posting it there would be the natural next step.

• On 1.28249... Lower Bound and Partial Upper Bounds for Cost-Preserving Single-Source Unsplittable Flows · 01 Aug 2026, 14:17 UTC

  Thanks, that's really useful context! So 1.28249 and so on is just where the explicit k=17 certificate lands, and the family should approach 4/3 as the number of terminals grows. Is the 4/3 limit established somewhere in the preprint (I could only find the 3/2 ceiling for the class), or is it numerical/expected for now? Happy to add it to the entry either way, I just want to label it correctly as proved versus conjectured. And if you ever certify a larger instance, the entry can track the new record constant.

• On 1.28249... Lower Bound and Partial Upper Bounds for Cost-Preserving Single-Source Unsplittable Flows · 01 Aug 2026, 12:22 UTC

  Feel free to discuss any entry values that might be wrong here. Also thank you for the submission :)

• On Non-Covering Congruence Systems over Fq[x] · 01 Aug 2026, 08:53 UTC

  Thank you Amber :)

• On Optimal Exponent Relating Sumsets and Difference Sets · 30 Jul 2026, 09:20 UTC

  Quite exciting to see a smaller model (295B) make contributions!

Recent edits

• Verification on Conway's Refinement Conjecture for Omnific Integers · 04 Sep 2026
• Verification on Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication · 03 Sep 2026
• Solve date on Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication · 02 Sep 2026
• Verification note on The Equality Case of Ehrhart's Volume Conjecture · 02 Sep 2026
• Verification note on The da Silva Machado-Seade Conjecture · 02 Sep 2026
• Verification note on The Near-Quadratic Elekes-Ronyai Expander Conjecture · 02 Sep 2026
• Verification note on Han and Jiang's Question on klt Type in Flat Families · 02 Sep 2026
• Verification note on Mauri and Moraga's Question on Log Calabi-Yau Pairs with Big Boundary · 02 Sep 2026
• Verification note on Shokurov's Global Index Conjecture for Foliations · 02 Sep 2026
• Verification note on Kollár and Kovács's Question on Cohomology of Fibers · 02 Sep 2026
• Verification note on The Ciliberto et al. Question on Effective Divisors of Positive Self-Intersection · 02 Sep 2026
• Verification on A tilted residue-class construction for long prime-free intervals · 30 Aug 2026
• Verification on Dean's conjecture for $k=5$ · 30 Aug 2026
• Verification on Haglund's Zero-Trajectory Conjecture for the First Riemann Xi Approximant · 26 Aug 2026
• Claim issue on Haglund's Zero-Trajectory Conjecture for the First Riemann Xi Approximant · 26 Aug 2026

Showing the latest 15 of 537.