3 ms·
Automating Mathematics PolyMath, Type Theory and Learning
- ur-whale 6y agoReally 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.