Speaking about large ambitious projects, Perelman's proof of Poincare's conjecture would be another. And it might push the formalization field quite a bit, because of the amount of modern geometry involved there.
Josef On Mon, 16 Apr 2007, Jesse Alama wrote:
Thought I'd forward this along to the mizar list, even though it superficially has to do with Coq. The web page mentioned in the message refers to mizar. Jesse