Who Can Understand the Proof? A Window on Formalized Mathematics

Stephen Wolfram discusses understanding proofs discovered using automated theorem proving. Based on Wolfram’s proof of the simplest axioms of logic of Boolean algebra.