Yes i talked about that in a different thread here. It has fishy ‘assume we have a lookup table for x’ assumptions in it. These are relevant to the main body of the loop. The numbers it deals with are outside of any possible lookup table capability (not enough atoms in the universe for such a table).

The lean proof uses these assume ‘a lookup table’ assumptions. The paper smells with the nlogn^0.99999999 (many more nines actually) and unbelievably close to nlogn statement and then the literal talk of lookup tables pushes it over the edge clearly for me.

Maths can generate weird numbers out of nowhere but it really really looks like an nlogn result with some tricks to get past leen to me

Just because something is proven and shown to be true doesn't mean that it's always practical.

The proof can be entirely valid even if it's not actually reasonable to implement and requires an enormous size lookup table - but it still is a meaningful mathematical result and makes progress.

I'm sure there are plenty of times where originally something was proven and thought to be completely impractical but then later had niche use cases or was the bedrock for solving other cases. And the opposite is true: there remain plenty of proofs of things that are mathematically certain but will in all practicality never be useful.

If the table size is constant, no matter how large, then it is correct and important (even if useless; the existing n*log(n) algorithm is already useless).