I fear I'm responsible for this misconception. At first we didn't realise the proof had originated on 4chan – Nathaniel Johnston originally found the proof on Wikia, and the 4chan archive was only discovered later.

When I tweeted about it, I said “The best known lower bound for the minimal length of superpermutations was proved by an anonymous user of a wiki mainly devoted to anime.”, by which I meant Wikia (which was pretty anime-centric at the time).

I think, combined with the fact that the problem was posed to 4chan in terms of Haruhi, and because it makes a funnier story, that the anime angle has been a bit exaggerated.

Having said that, the author of the proof is not (to the best of my knowledge) a mathematician, nor does he have any apparent desire to publish his result in a conventional form, so it's still a pretty unexpected place for such a result to originate.