Automating Mathematics PolyMath, Type Theory and Learning

Really interesting story of a new math proof starring, among others, Terence Tao.

But the meat of the story is not the proof itself, but rather how it was constructed and led to a wider program for CADTP (computer assisted theorem proving).

The first part (the proof itself) is interesting in itself, but the really cool part starts at ~ slide 20.