John Baez links to several letters from Grothendieck that have been posted on the Web. The most famous, of course, is Pursuing Stacks, which circulated for many years in photocopy form.

Scott Aaronson asks why mathematicians haven’t switched to machine-checkable proofs, and answers his own question by exhibiting the basically-human-unreadable proof of the irrationality of the square root of two using the HOL Light theorem prover. Scott provides a few interesting links:

• Adventures in the Verification of Mathematics, an essay discussing some of the issues by Harvey Friedman.
• Formalizing 100 Theorems, a list of a 100 candidate theorems for verification, and the systems that have verified them, by Freek Wiedijk.
• The Seventeen Provers of the World, a book-length comparison of different formalizations of the proof of the irrationality of the square root of 2, also by Freek Wiedijk

There is also the Flyspeck Project, a project to formalize Thomas Hales’ computer proof of the Kepler conjecture, which we mentioned once before.

There has been intensive discussion of Nasar and Gruber’s Manifold Destiny at Not Even Wrong, in these threads: Latest on Poincare, 2006 Fields Medal Winners, and Some Links. The controversy centers around whether Nasar and Gruber are unfair to Yau, but has taken an interesting turn: some of the commenters accuse the article of perpetuating stereotypes of Chinese mathematicians. The existence of a stereotype of Chinese mathematicians is news to me (ironically given the situation, there is a well-developed stereotype of Russian mathematicians that I have heard people invoke), so I’m curious if anyone else has ever heard any such stereotyping.

I see via Peter Woit that the American Institute of Mathematics (AIM), an independent mathematics research institute in Silicon Valley, is going to get a permanent in the form of a new $50 million dollar building modeled after Alhambra, a medieval Moorish castle in Grenada, Spain. AIM was cofounded by John Fry, the chief executive of Fry’s Electronics. (If you’ve never shopped at Fry’s, it’s like Home Depot for computers. They display computer parts the way a hardware store displays nails.)

Sylvia Nasar and David Gruber got the only media interview of Perelman, by dint of actually going to Saint Petersburg and asking him for one. But the real subject of their article in the latest issue of the New Yorker, Manifold Destiny, A legendary problem and the battle over who solved it, is Shing-Tung Yau, who (if the article is to be believed) has systematically downplayed the significance of Perelman’s contribution. Reading the article, it’s hard to figure out what Yau’s motivation would be: possibilities seem to be his friendship with Richard Hamilton, a desire to emphasize his own contribution or that of his proteges. The article also reports on a feud that Yau had with Gang Tian in Chinese newspapers.

I don’t have any first-hand knowledge of any of this (I had seen some rumors here and there on the internet, but I’ve seen rumors that Iran would nuke the United States as of yesterday, which demonstrates the incredible reliability of internet rumors), but if the article is right, then I do see one motivation for Yau that I would even find admirable (though probably wrong-headed): to fight the growing tendency of considering an theorem proven if experts can fill in the details. “Experts” can mean fewer people than can fill a jury. In theory, you could just become an expert, but in any sufficiently technical field there will be results that “everyone knows” but won’t be published anywhere, so unless you are part of “everyone”, it will be difficult for you to fill in the gaps without a great deal of rediscovery. (I don’t know if that is the case with Perelman’s proof.)

Perelman comes across better in the article than I had expected, though his motivation for turning down the Fields seems to be less because of otherworldliness, and more because he feels hard done by the mathematics establishment. Amazingly, he really does live with his mother, and is currently unemployed (though retired might be a better way to describe it). He claims to have quit mathematics, but without an actual substitute, it’s easier to quit smoking.

(The article quotes a post by an unidentified Brazilian blogger. On a whim, I tracked the quote down in Google to this post by Victor Rivelles.

Link to New Yorker article via an anonymous commenter to Scott Aaronson’s blog.

The 2006 Field Medalists have been announced:

Andrei Okounkov “for his contributions briding probability; representation theory and algebraic geometry.”

Grigori Perelman “for his contributions to geometry and his revolutionary insights into the analytical and geometric structure of the Ricci flow.”

Terence Tao “for his contributions to partial differential equations, combinatorics, harmonic analysis and additive number theory.”

Wendelin Werner “for his contributions to the development of stochastic Loewner evolution, the geometry of two-dimensional Brownian motion, and conformal field theory.”

The Nevanlinna Prize went to Jon Kleinberg, while the very first Gauss Prize was awarded to Kiyoshi Itō.

As was widely predicted, Perelman declined his prize, and did not attend the ICM.

What has caused more human misery, botulism or real analysis? Discuss.

Update. Before you answer, remember that botulism has given us less wrinkly foreheads.