s(7) is at least 5898

[Justin Lebar]

Hi, fellow Superpermutators.

Claude was able to put together a Lean-verified proof that 5898 ≤ s(7).

This improves upon the best lower bound that I'm aware of (from Vlad Gheorghe) by 2.

https://github.com/jlebar/superperm7-ge-5898

Please enjoy,

-Justin

[Benjamin Grayzel]

Hi Justin,

Cool! It looks like you've broadly adapted my (Fable/Sol-driven) approach for s(6)=872 to work for s(7) + the equality-cell argument. It's encouraging that Claude converged on the repo I released as the thing to build on, and reused as much of the machinery as it did. (Nothing wrong there, it's nearly entirely AI-generated hence the MIT license, but since you forked more than half of my repo--25 Lean files, 56% by bytes--to build from I did want to mention it). This can sort-of fall under my Lean audit, we've checked the same approach for s(6), though the s(7) statement itself is worth an independent check. Surgery.lean & Euler.lean specifically are general and fully covered, I can confirm those pieces.

One thing I'm curious about: was this Mythos? The copyright novelty isn't something I've seen before, your Claude cites Anthropic under Apache for all the files that weren't covered by my MIT license and you mentioned using an unreleased Anthropic model in the human note. If there's an Ant program that allows researchers to point unreleased frontier models at open problems I'd love to see what it does for the other bounds.

-Benjamin

[Miles Gould]

Cool! I did a bit of (AI-assisted) digging into this repo yesterday, and came to the following conclusions:

• In this repo, a "row" is a sequence of permutations connected by weight-1 edges, and a "trail" is a sequence of rows connected by higher-weight edges.
• It's basically a branch-and-bound search over the space of possible trails (or rather on "coarsened trail certificates", which I don't yet understand but I guess must shrink the space a lot?), recursing on the number of rows.
• The "shards" are contiguous slices of the search frontier after a certain number of recursions; the calculation that's done for each shard (a search showing that no point in that shard can lead to a successful completion of the search) is the same for every shard.
• For speed, this search is done at compile-time by Lean's native_decide tactic. This brings the Lean compiler into the trusted computing base.
• The sharding is also a speed hack, to allow greater compile-time parallelism.
• The per-shard files are generated by a Python script (tools/gen_cert.py), but this is not trusted: the theorem fsearch_false_of_shards in Superperm7/Cube.lean combines the per-shard proof certificates into a proof for the entire search frontier.

Does this match everyone else's understanding? It sounds like I should take another look at Benjamin Grayzel's proof first, to understand the certificates and the pruning strategy.

Incidentally, I was impressed by the unreleased model's writeup, which I found a lot easier to read than recent expositions we've seen from Sol and Fable. But it was still very terse and lacking in explanations of key terms!

Cheers,

Miles

--
You received this message because you are subscribed to the Google Groups "Superpermutators" group.
To unsubscribe from this group and stop receiving emails from it, send an email to superpermutato...@googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/313707ce-178f-45b0-8162-f5089ab0f5edn%40googlegroups.com.

[Justin Lebar]

> It's encouraging that Claude converged on the repo I released as the thing to build on, and reused as much of the machinery as it did. (Nothing wrong there, it's nearly entirely AI-generated hence the MIT license, but since you forked more than half of my repo--25 Lean files, 56% by bytes--to build from I did want to mention it).

Yes, and I specifically made sure we cited you!  Sorry if it wasn't prominent enough; I probably should have mentioned your name in my email.

> One thing I'm curious about: was this Mythos?

No, this is an unreleased Anthropic model.

> If there's an Ant program that allows researchers to point unreleased frontier models at open problems I'd love to see what it does for the other bounds.

I'm not aware of such a program!  If I find time I may indeed point this model at s(8) and so on, I bet it could make progress.  But first I have a few unrelated results sitting in my inbox.  :)  Nothing earth-shattering like what Levent has been doing, though.

I did push it to find a precise value for s(7), but that remained out of reach, at least with the amount of compute I was willing to throw at the problem.

[Benjamin Grayzel]

>Miles

I'm not sure about most of these, but 

native_decide sounds correct. It's a tactic that relies on machine code (using a script rather then doing the full axiom unfolding on a mechanical search, but still written in Lean and tied directly to the proof). It's a little dicier, if you wanted to cheat on a Lean proof exploiting native_decide is one of the easier methods, but it makes perfect sense to use here (for heavy search) and as long as the script isn't malicious we should be fine. My s(6) also uses native_decide.

'Per-shard files' from python also sounds right. Whenever I try to get AI to prove something it begins with a write-up + python, then Lean + python, then (when I force it) finally switches to pure Lean (or Lean + native_decide) but keeps the python scripts in the repo and just relabels them 'old' or something.

In my repo it's a 'run' that's a sequence of cost-1 edges, and a 'chain' is a sequences of 'runs' connected by cost-2 edges. I think 'row' is something slightly different but am unsure exactly what (Claude says "a cyclic interval of an insertion block")

>Justin

Yes! The repo has more than enough, thank you and sorry if my reply was pushy. I have the thought that it helps to know which AI-generations are more vs less similar as we try to digest them; wanted to show that our repos are credibly built on the same machinery (though yours customizes a lot for s(7): very different elimination techniques and at least one clean idea from Vlad's repo).

Cool! I'm going to go on a limb and assume you can't tell us anything like the model name :) or capabilities. If you have access to a beyond-mythos model though, honestly, I'm not sure I'd spend the tokens on s(8) or s(9). I give decent odds that an overnight highly parallel Sol/Fable run could already push those a little more, especially if told to grab/adapt whatever fits from current AI repos. If you want to spend tokens here, I'd shoot for a bound on general s(n) (ideally from a new/novel technique) or push harder on s(7). I'm pretty new to the problem though so I'd love to know what other people think.

-Benjamin

[Miles Gould]

On Mon, 17 Aug 2026 at 01:00, Benjamin Grayzel <benjami...@gmail.com> wrote:

'Per-shard files' from python also sounds right. Whenever I try to get AI to prove something it begins with a write-up + python, then Lean + python, then (when I force it) finally switches to pure Lean (or Lean + native_decide) but keeps the python scripts in the repo and just relabels them 'old' or something.

 

I think this is the Right Thing from an expository perspective, TBH: as a reader I would rather see where a proof came from than have it appear fully-grown as if from the forehead of Zeus :-) As long as it's clear which parts are scaffolding and which parts are crucial to the final proof.

 

In my repo it's a 'run' that's a sequence of cost-1 edges, and a 'chain' is a sequences of 'runs' connected by cost-2 edges. I think 'row' is something slightly different but am unsure exactly what (Claude says "a cyclic interval of an insertion block")

That sounds like the same thing to me - weight-1 edges cyclically permute their start points, e.g. 12345 -> 23451 - but you're right, I should make sure.

Cool! I'm going to go on a limb and assume you can't tell us anything like the model name :) or capabilities. If you have access to a beyond-mythos model though, honestly, I'm not sure I'd spend the tokens on s(8) or s(9). I give decent odds that an overnight highly parallel Sol/Fable run could already push those a little more, especially if told to grab/adapt whatever fits from current AI repos.

Good point - we've seen a lot of cases where weaker models are able to reproduce results from stronger models once they know where to look, so it seems likely that they could also build on those results.

 

If you want to spend tokens here, I'd shoot for a bound on general s(n) (ideally from a new/novel technique) or push harder on s(7). I'm pretty new to the problem though so I'd love to know what other people think.

I'm not sure! In general I think we care more about s(n) than about any particular instance of it, but I'm intrigued by the recent discovery that there are minimal-length superpermutations for n = 6 which contain repeated permutations. We've mostly assumed up until now that a minimal superpermutation had to be repeat-free, but this turns out not to be the case! So that suggests a new conjecture:

• Among all the minimal superpermutations for a given number of symbols, at least one has to be repeat-free.

and related questions like "what fraction are repeat-free?".

I'm also intrigued that Claude Anon extensively searched for 7-superpermutations of length 5905 and came up empty-handed - that suggests that Uku Raudvere's improvement to the Egan-Williams upper bound might be close to optimal. Which is somewhat surprising to me, since the E-W construction uses so little of the graph - only the weight-1 and weight-2 edges.

I posted a list of open problems back in 2019: Current open problems, aka "how can I help?" Excitingly, some of them have been settled within the last month! But as well as those already discussed above, I think the following might be interesting to take a crack at:

1. Is there some way of classifying the existing solutions for n in {5, 6, 7}?
2. Can we speed up Coanda's backtracking search any more, perhaps by taking greater advantage of the symmetries of the permutation graph?
   
3. Why do TSP solvers struggle with permutation graphs when they can handle much larger graphs in general? (It's entirely possible this one would succumb to a literature search, possibly even by a lower-end model)
4.  Can you prove that some edges (e.g. edges of maximum weight) are not needed for minimality?

HTH,

Miles