Physics Today recently published an interesting and thought-provoking Q&A with eminent mathematician Ken Ono, who recently took a leave of absence from his tenure-track position at the University of Virgina to join Axiom Math, an company developing AI tools to verify mathematical proofs. From the article’s opening paragraphs:
“Am I doing a better service to science by writing 20 more papers that only people in my field will read or by participating in this movement?” Ken Ono asked himself last year. At the time, Ono was an endowed chair at the University of Virginia. In the following months, he’d take a leave of absence from the university, move to Silicon Valley, and become the founding mathematician at an AI startup, Axiom Math.
Axiom is one of several companies focused on developing AI tools to verify mathematical proofs. In the future, similar tools could be applied to check AI-generated computer code, a potentially lucrative service now that AI tools can write lines of code faster than any human can debug them. Startups Harmonic and Math Inc as well as Google’s DeepMind are targeting similar AI-powered verification tools.
Axiom has attracted investor attention, reaching a valuation of $1.6 billion earlier this year. (Ono says that he has shares in the company and that he receives a salary that is similar to his former compensation at Virginia.) His interests, he says, are in helping researchers use AI to think in more-creative ways and across more disciplines.
Mean Green Math 