An independent, end-to-end Lean-verified candidate for s(6) = 872

[Benjamin Grayzel]

Hi all,

I'd like to present an alternative AI-elicited candidate for 872 at n=6. We are midway through a human audit of the technique; the math and approach seem plausible at a high level but the write-up has not yet undergone a thorough audit and I would love an outside opinion. The write-up was generated against an end-to-end formal verification in Lean 4 (https://github.com/BGray-wrl/superperm6). 

Because of the norms emerging around the erdős problems forum, I've been holding off on sharing this until I can independently check the result. However, given the current activity, sharing it now seems prudent. My early read indicates that Vlad and I have found approaches that, while similar at a high level, complement one another rather than compete (same hamiltonian-path formulation, different search reduction technique).

I'm working with an expert in formal verification to audit the Lean script; I can attest that the script compiles with zero sorries and no axiom declarations of its own or vacuous theorems, and to the best of my knowledge the problem statement has been formalized correctly - this covers the most common set of conditions under which Lean can fail.

In my own (no AI) words:
---
The system converted the permutation question into a graph minimization problem (where each permutation is one of 720 vertices and the connecting letters are edges). It then identifies that cost-1 edges create a partition of 120 6-cycles, notes a separate partition of 144 5-cycles, and uses structural constraints plus a 'genus identity' to reduce the full <=871-word search to 152 'combinatorial profiles.'

What remains is a messy case-wise evaluation and search through the 152 cases, which are individually ruled out through a combination of analytical arguments and programmatic evaluation. (Though I have an instinct that at least some of this messy case reduction was about reducing the complexity such that the agent could resolve the remainder on my personal computer and may not be strictly necessary).
---

I hope it's presentable! I’ve spent a while trying to understand this and shake it into a human-legible format. I’ve attached a one-page overview note here for a sanity-check. You can find a seven-page synopsis of the approach here alongside the full 18-page candidate write up.

-Benjamin

[Miles Gould]

Thanks particularly for the one-page overview! I see that both proofs use Euler's formula: could you explain how it arises in this context?

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/af7089c1-2779-47be-80b1-4f78a814a251n%40googlegroups.com.