A machine-checked improvement of the HPV lower bound

[Uku Raudvere]

Hi,

I’d like to suggest a lower bound: for all n ≥ 5,

S(n) ≥ n! + (n−1)! + (n−2)! + n − 3 + ⌈((n−3)!−1)/(2n−1)⌉,

i.e. HPV(n) + 1 at n = 5 and 6, then growing factorially:

S(7) ≥ 5886,
S(8) ≥ 46093,
S(9) ≥ 408289,
S(10) ≥ 4032273,
S(11) ≥ 43910408.


I’d like to start with caveats:

- I’m a software developer, not a mathematician.
- I’ve taken a course on basic combinatorics years ago and I don’t think I did too well.
- I can’t verify the proof myself.
- It’s an AI-generated proof.

This is the result of a side project where I wanted to see if I could use coding agents for proving nontrivial results. I didn’t expect it to work, but maybe it did successfully prove something. I’ve tried to find counterexamples or errors, but I’ve exhausted my ideas. I’m not planning on formally publishing the paper at the moment, as I’m not able to personally verify the result. The Lean formalization gives me a bit of confidence.


[AI summary]

The proof stays inside the HPV weighted-overlap-graph framework and keeps their three statistics: p (distinct permutations visited), c (completed cyclic classes), v (entered marked 2-loops). The HPV monovariant is rewritten as an exact identity

len(W) = HPV(n) + e + r + ℓ

with three nonnegative excesses. The entered 2-loops are ordered by first entry and compared against a canonical successor map of period n − 2; deviations are “breaks”, and

v ≤ (|A| + 1)(n − 2)

for |A| breaks.

The heart is a local analysis of break windows: every break not explained by a positive-defect edge deposits a charge on a rotation orbit shared by two entered loops; each shared slot receives at most two charges, and a slot receiving two forces two consecutive breaks whose intervening block has length 1 instead of n − 2, saving n − 3.

That compensation turns the coefficient 3 the raw charge count would give into a 2: for every k ≥ 0 satisfying

(2k(n − 1) + 1)(n − 2) + k(n − 1) < (n − 2)! + k,

one gets

S(n) ≥ HPV(n) + k + 1.

The criterion is linear in k and solves exactly to the ceiling above (the formalization also proves the ceiling is the most this criterion yields, and that the walk model is exact: Λ(n) = S(n)).

[/AI summary]

There is a PDF and a Lean formalization at:

https://github.com/urdvr/superperm-coeff2

As a side note: as side projects go, it was quite fun. Lots of dead ends. I learned quite a bit about (potentially, somewhat) effective ways of using the current models and tools.

[Ranbir Das]

Hi,

Thanks for sharing this. I found it particularly interesting that the argument stays entirely within the HPV weighted-overlap framework rather than introducing a completely new construction. The idea that a more refined local analysis of "breaks" can improve the coefficient from 3 to 2—and thereby strengthen the lower bound—is an intriguing approach.

I also appreciate your transparency regarding the AI-assisted development and the Lean formalization. It's an interesting example of using AI as a research collaborator while still relying on community scrutiny for mathematical validation.

Out of curiosity, did the AI primarily help discover the argument, or was its larger contribution in organizing and formalizing ideas that had already emerged?

Thanks again for sharing your work. I'll be interested to see what the group thinks after people have had time to read through the PDF and Lean development.

--
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/d8207b28-840d-4348-bc08-e5c36dbd245an%40googlegroups.com.

[Uku Raudvere]

This is a fully AI-generated result. I wanted to learn how to aim a (system of) agent(s) at a problem and how to structure their workflow so it remains productive. Because my main goal wasn't necessarily to reach an interesting new result, I didn't give the AI any specific ideas as a seed. I also didn't explicitly give it any prior work, but it was free to search for papers online.

So - I want to be clear - I had no creative input into the direction or structure of the (potential) proof. The AI was free to use any approach it could come up with. I mostly observed the work as it proceeded and patched and updated the process whenever I saw recurring errors or plateaus. Despite my best efforts, I never got the process to run fully autonomously for more than 12 hours or so. Every now-and-then it needed encouragement to "continue with the most likely path forward" or "think for a while and try to come up with ideas you haven't tested yet". Purely mechanical solutions all eventually got stuck in dead-end loops.

The eventual output was a swath of Lean-formalized lemmas and theorems, many of which were dead ends. When it found an actual potential result, I had it push it as far as it could easily go, had it write up a paper, reprove the theorem cleanly to match the architecture of the paper and get rid of the structures that were shaped mostly by the search process.  

[Miles Gould]

I've added a Dockerfile to make it easier and safer to compile the Lean code (https://github.com/urdvr/superperm-coeff2/pull/1), and I can confirm that the code compiles cleanly and only reports the use of the axioms [propext, Classical.choice, Quot.sound] as claimed. I haven't yet read the paper or properly checked the formalisation of the theorem.

Has anyone else got any further?

Miles

To view this discussion, visit https://groups.google.com/d/msgid/superpermutators/0f94e0f0-d328-4928-a149-d22e11344b84n%40googlegroups.com.