We begin in 1982 when Ravi Kannan proved that Σ2 (the problems computable in NP with an NP oracle) cannot have n2 size circuits. Kannan's result hold for nk-size circuits but for this story we'll keep it simple.
Kannan had an ingeniously simple proof. By diagonalization you can create a language L in Σ4 that does not have n2-size circuits. Now there are two cases:
- SAT doesn't have n2-size circuits. Since SAT is in Σ2 we are done.
- SAT has n2-size circuits. Then by Karp-Lipton Σ4 = Σ2 so L is in Σ2 and we are done.
Kannan's proof is non-constructive and doesn't give an explicit Σ2 language that we can show doesn't have n2-size circuits. Either SAT or L but one can't be sure which one.
In 1998, Sunny Daniels, a PhD student at Rutgers, took Eric Allender's complexity course. Eric offered up a constructive example of Kannan as an open problem. Sunny came up with a solution. He wrote up a draft in LaTeX but for personal reasons dropped out of academics and never published the paper.
In 2003, Jin-Yi Cai and Osamu Watanabe, not aware of Daniels' paper, came up with their own independent construction and presented their paper at the COCOON conference in Montana. Word got back to Sunny but he thought he had lost the LaTeX file and didn't want to retypeset the whole proof.
Sunny had Iomega Zip Drive cartridges from his Rutgers days. Recently he found someone who had a Zip Drive reader and managed to recover the files. In there he discovered the original LaTeX, cleaned the paper up, and sixteen years after his proof put the paper on ArXiv. Even if you don't care about the math, read the introduction for the complete version of this story.
Kannan's proof actually shows Σ2∩Π2 does not have n2-size circuits and this was later improved to S2P. Whether we have any constructive language in Σ2∩Π2 or S2P without n2-size circuits still remains open.