This reminds me of a fun experience I had in grad school. I was working on writing some fast code to compute something I can no longer explain, to help my advisor in his computational approach to the Birch and Swinnerton-Dyer conjecture. I gave a talk at a number theory seminar a few towns over, and was asked if I was doing this in hopes of reinforcing the evidence behind the conjecture. I said with a grin, "well, no, I'd much rather find a counterexample." The crowd went wild; I've never made a group of experts so angry as that day.

Well, I never was much of a number theorist. I never did come to understand the basic definitions behind the BSD conjecture. Number theory is so old, so deep, that writing a PhD on the topic is the step one takes to become a novice. Where I say that I didn't understand the definitions, I certainly knew them and understood the notation. But there's a depth of intuition that I never arrived at. So the uproar of experts, angry that I had the audacity to hope for a counterexample, left me more curious than shaken: what do they see, that they cannot yet put words to?

I am delighted by these advances in formalism. It makes the field feel infinitely more approachable, as I was a programmer long before I called myself a mathematician, and programming is still my "native tongue." To the engineers despairing at this story, take it from me: this article shows that our anxiety at the perceived lack of formalism is justified, but we must remember that anxiety is a feeling -- and the proper response to that feeling is curiosity, not avoidance.