If we refine the question to something like "Who would be most successful in leading a campaign to automate proof-checking in huge swaths of mathematics?", then I'll start the bidding by nominating David Mumford. His experience as an algebraic geometer makes him eminently qualified to assess just how deep mathematics can get, and his more recent work with computer vision makes him credible as an authority on what current methods of automation might be able to achieve. Don Knuth would also be plausible as the leader of such a automation crusade. As a computer scientist, he has a keen understanding of what it takes to create a software system. And, to the extent that his personal style and his sense of design contributed to the success of TeX, one might predict that he'd use the same flair to develop and promote a general- purpose proof-verification system for mathematicians. If the impulse behind the question is "Who's the one person in the world such that, if I convince him, he'll convince everyone else?", there's a catch: It could be that the more qualified someone is to say "This is something we mathematicians can and should do" and get people to take notice --- that is, the more knowledgeable he/she is about what math is, and what early 21st century computers can do --- the less likely it is that he/she would say it. Jim Propp