The speaker thinks formalizing familiar mathematics for computer checking encourages mathematicians to represent concepts and combine them more efficiently.

“And I think what they liked about it was, you know, when you go back to a piece of mathematics that you think you understood, but now you have to represent it formally, you have to represent it in a way that the computer can, can understand and check every detail, you find yourself getting very efficient about how you represent concepts and put them together.”