Look and Say Sequence; the one that's like 122111 → "one one, two twos, three ones" → 112231. I have a special place in my heart for that sequence even more so recently since it showed up in the last Puzzlestorm — to solve the puzzle you had to unapply the operator, twice. Despite the groaning of everyone at the debriefing who didn't solve it, I thought it was a cute puzzle. Anyhow
The analysis of this sequence is delightfully ridiculous (one might more generously say "fanciful"), as only someone like John H. Conway could pull off. The main lemma is called the "Cosmological Theorem", and says that any string of digits eventually decomposes into "atoms", some of which are "common", and some of which are "transuranic". After that point all atoms don't "interact" with one another, and the problem of asymptotic density of atoms can be handled by a 92-element transition matrix — the 71-degree polynomial pops out of eigenanalysis of that matrix. Both original proofs of the Cosmological Theorem were lost, but it was reproven by Doron Zeilberger, and a tighter bound was achieved by Rick Litherland.
Both proofs rely considerably on computer calculations — Zeilberger (in the right spirit of things, I think) even went so far as to list his computer (!) as first author on the paper. I wonder if these are nice bite-sized (compared to such smörgåsbordic problems as the Kepler conjecture) problems for proofs of program correctness?
Also while looking up how to spell smörgåsbord I found that Swedish has this insane phoneme that some linguists don't believe exists, quite. Man this is like the pulmonic ingressive uvular trill (aka "voiced snore"), except for real.