[stevenwu]

not too long ago I attended a talk by Thomas Hales (proved the Honeycomb conjecture and the Kepler conjecture) where he talked in detail about his Flyspeck project, which he says has just a 400 line kernel that traces every line of a proof down to the axioms, that will formalize his proof of the Kepler conjecture and many questions in the Q&A after had to do with curiosity of machines being able to do exactly this. very interesting