Abstract
Mathematician Akshay Venkatesh recently wrote an essay on the possible effect on mathematical practice of advances in automatic theorem proving, and in particular on our value judgments about theorems. I will argue that if computers become capable of proving interesting theorems, then they will have to make value judgments for themselves, and that these judgments will reflect objective properties of the vast network of well-formed mathematical statements, just like our own.
