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).