Vladimir Voevodsky is a math superstar who plausibly could acquire such an interest.
Here is a summary of a recent talk he gave. After winning the Fields medal in 2002 for his work on motivic cohomology, he felt he was out of big ideas in that field. So he “decided to be rational in choosing what to do” and asked himself “What would be the most important thing I could do for math at this period of development and such that I could use my skills and resources to be helpful?” His first idea was to establish more connections between pure and applied mathematics. He worked on that for two years, and “totally failed.” His second idea was to develop tools/software for mathematicians to help mathematicians check their proofs. There had already been lots of work on this subject, and several different software systems for this purpose already existed. So he looked at the already existing software. He found that either he could understand them, and see that they weren’t what he wanted, or that they just didn’t make any sense to him. “There was something obviously missing in the understanding of those.” So he took a course at Princeton University on programming languages using the proof assistant Coq. Halfway through the course, he suddenly realized that Martin-Lof types could essentially be interpreted as homotopy types. This lead to a community of mathematicians who developed Homotopy Type Theory/Univalent Foundations with him, which is a completely new and self-contained foundation of mathematics.
Andrej Bauer, one of the Homotopy Type theorists, has said “We’ve already learned the lesson that we don’t know how to program computers so they will have original mathematical ideas, maybe some day it will happen, but right now we know how to cooperate with computers. My expectation is that all these separate, limited AI success, like driving a car and playing chess, will eventually converge back, and then we’re going to get computers that are really very powerful.” Plausibly, Voevodsky himself also has some interest in AI.
So here is a mathematician with:
a solid track record of solving very difficult problems, and coming up with creative new insights.
good efforts to make rational decisions in what sort of mathematics he does, yielding an interest and willingness in completely switching fields if he thinks he can do more important things there.
an ability to solve practical problems using very abstract mathematics.
I think it would be worth trying to get him interested in FAI problems.
Vladimir Voevodsky is a math superstar who plausibly could acquire such an interest.
Here is a summary of a recent talk he gave. After winning the Fields medal in 2002 for his work on motivic cohomology, he felt he was out of big ideas in that field. So he “decided to be rational in choosing what to do” and asked himself “What would be the most important thing I could do for math at this period of development and such that I could use my skills and resources to be helpful?” His first idea was to establish more connections between pure and applied mathematics. He worked on that for two years, and “totally failed.” His second idea was to develop tools/software for mathematicians to help mathematicians check their proofs. There had already been lots of work on this subject, and several different software systems for this purpose already existed. So he looked at the already existing software. He found that either he could understand them, and see that they weren’t what he wanted, or that they just didn’t make any sense to him. “There was something obviously missing in the understanding of those.” So he took a course at Princeton University on programming languages using the proof assistant Coq. Halfway through the course, he suddenly realized that Martin-Lof types could essentially be interpreted as homotopy types. This lead to a community of mathematicians who developed Homotopy Type Theory/Univalent Foundations with him, which is a completely new and self-contained foundation of mathematics.
Andrej Bauer, one of the Homotopy Type theorists, has said “We’ve already learned the lesson that we don’t know how to program computers so they will have original mathematical ideas, maybe some day it will happen, but right now we know how to cooperate with computers. My expectation is that all these separate, limited AI success, like driving a car and playing chess, will eventually converge back, and then we’re going to get computers that are really very powerful.” Plausibly, Voevodsky himself also has some interest in AI.
So here is a mathematician with:
a solid track record of solving very difficult problems, and coming up with creative new insights.
good efforts to make rational decisions in what sort of mathematics he does, yielding an interest and willingness in completely switching fields if he thinks he can do more important things there.
an ability to solve practical problems using very abstract mathematics.
I think it would be worth trying to get him interested in FAI problems.