If you want America to regain the place it had in the middle of the twentieth century, you need to make it an attractive place for the top foreigners to relocate to. Stop importing people to fill up jobs at the bottom and middle, and start importing world leaders again.
It is rather hard to make someone who is a "top foreigner" to relocate. People need strong reasons to move permanently to a different country. The situation that made Einstein and Von Braun come to America was rather exceptional and unlikely to happen again. The real reason for millions of smart people to emigrate to the USA in the second half of XXth century was the difference in the standard of living between the USA and their home countries. Some of those people became "top" and contributed to American lead in technology. But this difference in standard of living is disappearing and there is no way to stop that. I am sure though that making it easier for foreigners to get permanent resident status after obtaining a PhD from an American university would slow down the reverse brain drain. I speak from experience here - it took me 14 years to get my Green Card. If I had gooten it after say 6 years, around the time I got my PhD, we (my wife, a PhD in biology and I) would still live in America. But the US forced us to keep our options open and when the opportunity showed up last summer we moved back to our home country.
Do we cure an alcoholic by offering him even more of his favorite beverage?
Interesting analogy. I always thought that stimulating the economy with borrowed money is like drinking vodka to warm up in freezing weather. Maybe it even helps, but the risk is that you are likely to keep doing it when the times are better and after some time you just can't stop.
Peer review is typically anonymous
Apart from a couple of experiments, peer review is never anonymous. It is typically half-anonymous - the author does not know the identity of reviewers, but the reviewers do know who is the author. I don't know in other disciplines but in mathematics this is a necessity from the practical point of view. Active researchers may get more than one paper to review per week. Sometimes one would need a couple of weeks to check all the details in proofs. So the reviewers have to rely on the credibility of the authors and the institutions the authors are affiliated with to make a judgment.
It's like trying to describe to someone a book by describing which pixels are black and white on the page.
Very good analogy, thank you. This is what someone who knows only about printing press would say about impossibility of showing text on a computer screen - "imagine the work that would have to be done to split the image into pixels and then put them together so that they don't look like gibberish".
Formal proofs are (...) nowhere near able to handle genuine problems in mathematics.
If you really want you can always make this statement true by selecting the right definition of "genuine problems", for example defining genuine problems as those that have not been formalized yet. Otherwise you may want to check the list of top 100 of mathematical theorems to see which ones have proofs written in a formal proof language.
Unreadable by humans: there's no point.
Here you have a point. This proof is not designed to explain to a human why the theorem is true. It should not be called a proof, it should be called a verification script. But this is just an unfortunate choice of the language. There are other proof languages that are designed to be readable by humans.
CS at least potentially has a built-in reality check that pure math lacks.
There is such check: writing proofs in a formal proof language so that they can be verified by a machine. This is a barrier high enough that no crackpot can jump over it. Too bad math departments don't teach formal proof langauges.
Readability and writeability are separate and diametrically opposed issues. (...) We apparently both agree that readability and writeability are conflicting goals.
Not exactly. My opinion is that readability and writeability are orthogonal in the design of a formal proof language. For most formal proof languages the design effort was invested in writeability because those languages were intended to be used for formal verification of software. However, mathematicians are not only interested in the fact that the assertion of a theorem is true, but also want to know why it is true, i.e. they want to be able to read the proofs. There is a line of formal proof languages whose design goal is readability (Mizar, Isar and the declarative proof language for COQ ). After getting used to, proofs in those languages are as readable as standard (informal) proofs.
machine readable proofs are not useful for developing new math, and they are also not useful for teaching mathematics to the general public
Well, if you phrase it this way I agree. Writing formal proofs will always be more difficult than writing the standard ones. This is because they contain much more information. It is not useful for a mathematician to write his/her proofs in a formal proof language before publication. In most cases it is not even practically possible because there is not enough background in formalized form. So, if you are a mathematician, formalized mathematics will not be of much use. It will not advance your career. It may inhibit it as it is a bit addictive and may consume the time you should spend writing publications and grant proposals. It is also not useful for educating general public. It typically requires some background in the foundations, like set theory. General public doesn't know set theory. General public doesn't know how to add fractions. So what is formalized mathematics good for? I personally do it for fun and as expression of creativity. I think it may be useful for getting more information about existing mathematics. For example, take the role of the axiom of choice in the construction of Lebesque measure. Since in ZF you can not prove that real numbers are not a countable union of countable sets, you can not construct the Lebesque measure (or any nontrivial measure on real numbers that assigns zero to all singletons) without using the axiom of choice somewhere. Where exactly is it used? What can you get without it? It would be very easy to find out if we had a formalized construction. Another use of formalized mathematics could be learning mathematics not by the "general public" but by the students of mathematics. We may disagree on that since you don't believe that formal proofs can be made readable. But I think they can, and if they are structured well, as Isar allows, the machine can display the desired level of detail, zoom in if some step is not clear and zoom out if some part is (seems) obvious. This use is more about knowledge representation than correctness of proofs.
In these matters the only certainty is that there is nothing certain. -- Pliny the Elder
