s(8) >= 46,130 per GPT-6 Astra

[William Echols]

Using the recent GPT-6 model with Extra High effort, I obtained a lean verified proof of s(8) >= 46,130. I had previously been working with GPT-5.6 Sol to improve this bound, but it was unable to do so. As always, additional review would be appreciated.

Github repo with lean proof: https://github.com/williamechols/superperm8-ge-46130.

I merely provided the following prompt in codex, and later asked for formalization:

Your goal is to advance the minimal superpermutation problem. The latest updates, including explicit upper bound constructions and lower bound proofs, can be found on the Superpermutators Google group. You may choose to either extend an existing result, or consider a new approach. We will need be thoughtful and consider the problem in a new light to find this improvement on this hardware.

This result relies heavily on the work of Lebar (https://github.com/jlebar/superperm7-ge-5898) and Grayzel (https://github.com/BGray-wrl/superperm6).

[Miles Gould]

Cool! I've added a "best lower bound" column to the spreadsheet (https://docs.google.com/spreadsheets/d/1m8mHizDHoDpT-9ohCiqmfKyQI6gmhuyuzb7TC7362Ko/edit?usp=sharing) and added this and Lebar's results.

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/e0a79021-8d14-4432-ba1a-918de22a18acn%40googlegroups.com.

[Ranbir Das]

Thanks Miles — this updated table is very useful for seeing where the lower-bound and construction results now stand, with William’s new Lean-verified (S(8)\geq 46,130) result incorporated. 

One aspect I find especially interesting is how the “best lower bound” is progressing relative to the best constructions: it makes the remaining gap much more concrete. I’m also interested in the underlying notion of greediness here — where a local minimum means choosing the cheapest available transition at each step, but the important question is whether those individually optimal choices can remain globally compatible rather than forcing a later penalty. The fact that some of these bounds are now being pushed through machine-verified proofs makes this increasingly interesting as a computational research problem, particularly in understanding where local optimality can actually translate into a stronger global constraint.  

Ranbir

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