n=8 superpermutation of length 46204

[Uku Raudvere]

https://github.com/urdvr/superpermutation-examples/blob/main/superpermutation-8-46204.raw.txt

I didn't find examples of this, I think it's novel. 

[Theo H.]

Uku,

According to all my tests, this superpermutation is valid and one shorter than the known Egan length (46205).
You should submit a pull request to add your superpermutation to https://github.com/superpermutators/superperm (this is the corpus I have been using)
Well done! I was reading your paper and it seemed very logical, the argument was well formulated.
There are a lot of similar constructs appearing between your work and mine. I think your theoretical work is also correct, for what my opinion is worth.

Best,
Theo H.

[Robin Houston]

This works, and it is indeed new!

Can you explain how you found it? If any search was involved, can you share the code used to perform the search?

Cheers,

Robin

On Sun, 26 Jul 2026 at 18:06, Uku Raudvere <u.rau...@gmail.com> wrote:

https://github.com/urdvr/superpermutation-examples/blob/main/superpermutation-8-46204.raw.txt

I didn't find examples of this, I think it's novel. 

--
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/6f2f7202-9694-4813-99fc-ea1da06599aen%40googlegroups.com.

[Robin Houston]

PS. This seems to be a tree-like superpermutation with a standard kernel (consisting of the principal 3-cycle), and 833 2-cycle extensions, each contributing 6 new 1-cycles, in a tree as shown in the attached text file.

This lends yet more weight to the conjecture that such superpermutations exist for all n.

It would be great if the method used to find this could shed any light on the general case!

[William Echols]

Hello,

After reading this thread, I became interested in determining if GPT-5.6 is capable of improving the upper bounds for other dimensions. In a ~2 hour session with GPT-5.6 in Codex, I obtained what I believe to be a length 408,965 superpermutation for n=9, and a length 4,037,046 superpermutation for n=10. Interestingly, both are 1 shorter than Egan's general construction.

The files are available at this Github repo: https://github.com/WilliamEchols/superpermutations.

I will review the methodology in more detail and provide a write-up soon. Also, I would greatly appreciate independent verification.

[Theo H.]

Hello William,

I checked both of your superpermutations and they are indeed valid, novel superpermutations. Congratulations!!!
Though you'll have to take my word for it, I was working at the same time as you, and it seems we independently discovered the same kernel. I have taken the liberty of pasting below.

I am interested to read your write up!

8/12345679 8/92345671 8/29345671 8/23945671 8/23495671 8/23459671 8/23456971 9/12345678 1/92345678 1/29345678 1/23945678 1/23495678 1/23459678 1/23456978 9/82345671 1/82345679 1/89345672 1/83945672 1/83495672 1/83459672 1/83456972 9/28345671 1/28345679 1/98345672 1/38945672 1/38495672 1/38459672 1/38456972 9/23845671 1/23845679 1/93845672 1/39845672 1/34895672 1/34859672 1/34856972 9/23485671 1/23485679 1/93485672 1/39485672 1/34985672 1/34589672 1/34586972 9/23458671 1/23458679 1/93458672 1/39458672 1/34958672 1/34598672 1/34568972 9/23456871 1/23456879 1/93456872 1/39456872 1/34956872 1/34596872 1/34569872

[Uku Raudvere]

I generated some more words at different n and added them to my repo along with the generator code. I think they might not reproduce perfectly - I didn't keep rigorous notes about the specific code I used as it evolved. But it should vaguely reproduce. https://github.com/urdvr/superpermutation-examples

 I have Williams words in the repo as well as they were very useful for analyzing the construction structure.  

The generator should give new constructions with different seeds.
In general, it seems I can generate a -1 word from the Egan recursive construction. I can perturb -1 walks to get different structures. I can usually (but not always?) lift an n-alphabet -1 walk to n+1

For example, recursively lifting from n=10 gives words of
n=11 43948807
n=12 522910088

I also have n=13 at 6,749,568,009, but it's too large to easily fit GitHub. I assume it can be lifted indefinitely.

[Robin Houston]

Amazing! If we can prove it can be lifted indefinitely, that will give the upper bound that we have long conjectured.

I wonder if this can be adapted to find even shorter superpermutations by using a different kernel, as we were able to do for n=7.

Robin

--
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/71fcd587-eca8-49e4-b649-86afb27b9061n%40googlegroups.com.

[Theo H.]

I am strongly of the opinion that this can be lifted indefinitely, even the 5906 2-window savings.

I included some code that might help with systematic compression. It might be more work than using an archive, but maybe it will be of use to someone.

It takes advantage of the "clean" appends which can be made without introducing a waste symbol. The encoding scheme basically just records how many symbols elapsed before waste, and the index (relative to n symbols ago) the waste was appended from. I didn't think it was gh worthy yet (no comments and clean code) but I declare anybody free to use it under copyleft.

These Charlie vane type constructions don't use complex appends of strange indexes so you should be able to see a reduction of symbols by 1/n. Still not as efficient as using a binary file format but someone else is still free to do that.

Please let me know if you have any questions

[Uku Raudvere]

I think I have a proof that there is a lift for any n>=8. Or specifically, there are specific walks that can be lifted indefinitely.

Lean proof, example of a superpermutation that can be lifted, write-up and .cpp code for lifting it are at:

https://github.com/urdvr/superpermutation-examples/tree/main/formal

[Miles Gould]

I see that a recent claimed disproof of the Collatz conjecture actually turned out to be exploiting a bug in the Lean kernel: Kernel accepts wrong-structure projections, allowing an axiom-free proof of False · Issue #14576 · leanprover/lean4. Worse, it was simultaneously exploiting two independent bugs in two different Lean implementations, so neither caught the error! #lean4 > Counterexample to the Lean Conjecture (Soundness Bug) - Lean - Zulip

This feels more like an exploit chain than an honest error to me, and suggests that we should treat AI-generated Lean proofs with more caution. Does anyone have any suggestions as to how? I suppose we could check submitted proofs against the latest Lean and nanoda nightly versions, and run AI audits against them with instructions to look for Lean exploits. I don't think manual checking is viable - I for one am not a Lean expert; I haven't even managed to check the formalisation of Uku's first submission yet; and since then several more results have landed!

Miles

To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/62198e54-9bea-4676-b2f8-9a0fb72c87c7n%40googlegroups.com.

[Robin Houston]

If this is a deep philosophical question, I don’t have anything useful to say. If it’s a pragmatic question, I expect Lean soundness bugs to be found and fixed over time, and so if a Lean proof continues to pass as new versions of Lean are released then personally that will increase my confidence in its correctness.

(I would also hope for the number of soundness bugs in the Lean kernel to tend to zero over time, but we shall have to wait and see whether that’s the way things turn out.)

Robin

To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/CAKFNCm1sOfPejWo6SvNoEhoTbgxLnv%2BXjerYpOgCfis82vUFow%40mail.gmail.com.

[Miles Gould]

This is a purely pragmatic question. 

Another possibility would be to publish a preferred Lean formalisation of the problem on the main superpermutations repository, and ask submissions to use that rather than formalising the problem from scratch. This would guard against formalisation error, but not adversarial "proofs" that exploit soundness bugs in Lean.

[Uku Raudvere]

I'm more worried about formalization errors than soundness bugs in Lean. I think it's unlikely for an agent to accidentally stumble on an error when working toward a real proof. The AI doesn't try to achieve a maliciously compliant false proof, but is working from plausible mathematical hypotheses. Especially when lemmas only proceed after the idea has been computationally tested and didn't get rejected by a counterexample.

Formalization errors could be more insidious. I'm somewhat worried about correctly proving the wrong true theorem due to an initial formalization errors. I try to mitigate the risk by generating a paper from the Lean proof and having it evaluated by the strongest models I have access to without giving them the Lean code as context.

[Ranbir Das]

It's been interesting to see the discussion being taken forwards from several different angles.

One thing I kept thinking is whether it would be useful to build tooling around the walks themselves - For example, annotating each transition with the overlap it contributes, comparing kernels step-by-step against existing constructions, or automatically highlighting where the "-1" saving is actually achieved. It feels like that could make it easier to understand why a particular kernel works, where two constructions diverge or involve experimenting with new kernels to be better involved.

To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/9acee5f7-cc67-4e9f-bce4-5890b68ca7ecn%40googlegroups.com.

[Miles Gould]

Go for it! There are a couple of visualisation scripts in the bin/ subdirectory of  superpermutators/superperm, but there's definitely scope for more.

To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/CACNkbk-6vyx4K3wGFicrQ1mjbsQrfyDtVZ%2BqY%2BcRpqtfBstn7A%40mail.gmail.com.

[Jay Pantone]

LLMs have definitely been known to "reward hack" and accomplish their goal of proving something in Lean by finding bugs, or sneakily misstating theorems or smuggling in axioms. My feeling is that since I don't know Lean myself, to have very strong confidence in a result whose proof contains a lot of details and moving parts (like proofs of lower bounds for superpermutations tend to have), I would need both of (1) a well-written article with all the details of the proof, and (2) a Lean formalization of it, audited by a capable model. 

Regarding (1), I find most AI writing completely impossible to read. It tends to be full of unnecessary jargon used to hide details. AI can be a capable writing assistant, but in my experience if the human guiding it doesn't understand every detail, then the article won't be effective at communicating them. As for (2), I find GPT 5.6 Sol, used in codex, to do a good job testing Lean formalization, searching for holes, extra axioms, checking the theorem itself is formalized correctly, etc. It might not catch if a bug was subtley used. Having it use Comparator and Nanoda help too.

I've had some codex instances trying to audit some of the new results, particularly the claims that prove 872 is optimal for n=6. Unfortunately I don't have the time it would take right now to read the accompanying articles, but I find codex's mathematical judgements to be pretty reliable after you've really pushed at it. I'll try to post results when I can (but I should be clear that I'll be posting codex's judgements, not my own!)