I don't think you ever met personally any people who returned to their home country from the USA. I have met a couple of them (and I am one myself) and the tendency among them is rather to dislike America. I call it a "Pol Pot syndrome".
It's not necessarily something "very wrong" that USA did, it's just that China is catching up and the reasons for leaving the family, adjusting to a different culture and starting from close to zero in America are disappearing. This will accelerate in the future, especially when the realization that the US is a bankrupt country sinks in (heard that laughter when Geithner told Chinese students that dollar assets are safe?).
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.
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 order for this claim to be true (...) one would at a minimum need to be able to efficiently write existing proofs in the formal language
I don't quite follow your reasoning. In order to convince you that some proof languages are readable I would need to be able to write formal proofs efficiently? Ease of writing formal proofs is not much related to readability. As I mentioned, languages that are designed to make writing the proofs easier tend to be less readable. For some examples of machine verified proofs that I consider readable you can look at the Tiddly Formal Math site (disclaimer: I am the author of that site).
As for what will be formalized in someone's lifetime it's a moving target. People used to say that the prime number theorem will not be formalized in their lifetimes and many were wrong.
I am happy that the proofs being mentioned in this type of argument now are much more recent.
I think formalizing large areas of mathematics will advance the development of new mathematics in about the same extent as development of modern foundations of mathematics at the end of XIX century. It was not obvious to see at that time as well why there was even a need, and how it would help.
anyone who's ever seen a machine-verifiable proof knows that they're even more obfuscated than perl code
How many formal proof languages have you seen? Most of them are designed for software verification, not formalized mathematics. They are optimized to make it easier for the author, not for the reader. Vdash will (probably) use Isar which is as easy to read for a mathematician as a standard proof. There may be an excessive amount of detail that sometimes obfuscates the big picture, but there are ways to deal with that, too.
Mizar library would be an attractive target to import. It is the best library of formalized mathematics in existence. The problem is that then you would have to make Mizar the back end of the wiki, but Mizar is not free software.
Writing an alternative parser for the Mizar language would be very difficult, people have tried to do that and failed.
Also, there are copyright issues with trying to import the Mizar library.
A problem with Metamath is that it is very labor-intensive to develop proofs.
This is not the only problem. Another one is with the readibility of the proofs. Mathematicians want to know why theorems are true. Trying to understand a Metamath proof is like trying to understand an algorithm by reading assembler code.
An ideal solution would be a high level formal proof language (like Isar) with a theorem prover that "compiles" it to Metamath for independent verification.
we need to integrate formal proof software concepts
I am very happy to hear that. Maybe this will result in a decent authoring and presentation tool for Isabelle.
Mathematics is not about calculations, it is about theorems and proofs. I would not call any software "math software" if I can not do math with it (i.e. write a proof and verify it). This is not to criticize Sage which I consider an awesome piece of software engineering, mostly because of using existing excellent tools rather than inventing its own.
Why is the plaintiff's age important enough to be mentioned in the judgment? How old one has to be to not be "young" in the eyes of the German legal system (apparently more than 33)? Is this special treatment of adult "young" people peculiar to Germany or happens in other European countries? If I am annoyed by this, does that mean I am old?
As a former mathematician I am always surprised by mathematicians who think that the natural number 4 (that is the set {0,{0},{0,{0}},{0,{0},{0,{0}}}} ) should be equal to any real number (which are usually some sets of Cauchy sequences or Dedekind sections of rational numbers).
As a high tech worker with two PhDs who is about to move back to my home country because my green card application got stuck in a 300,000 people long que at the "Backlog Elimination Center", I couldn't agree more.
Of course every country has right to set its immigration policy. However, a policy that gives the preference to farm workers rather than highly educated people is clearly suboptimal in the long term.
>What am I missing here?
A couple of things. For me writing software (or formalized mathematics, which is quite similar) is an expression of creativity, like writing poetry or painting. I am willing to do it without hope of ever making money on it.
Another thing you are missing is the big picture of efficiency of writing software the proprietary vs. open source way. I once had to write a Windows and Linux driver for the same board that my company makes. Windows driver: 12000 lines of code. Linux driver: 200 lines patch submitted to kernel.org. How was that possible? Well, in Windows I had to implement everything from scratch. In Linux, the support for the chip was already there and I only needed to code some stuff specific to the board. Yes, it would be possible to buy some "intellectual property" for the Windows driver that would make the task easier. However, the very cost of the transaction (just the effort to find the vendor, negotiate agreement etc) would exceed the cost of effort needed for the Linux driver.
I think the factor of efficiency will become more and more important as software becomes more and more sophisticated.
Yes, I am quite happy with my account at cosmopod.com "internet operating system" - a full remote KDE desktop delivered from UK to CA with NX protocol. It is faster to use KDE or firefox this way than locally on my 6 years old machine.
There are tradeoffs related to privacy, but those may depend on the country you live in. Sometimes your data are safer when physically located in a different country than your machine at home.
Slashdot Mirror
I don't think you ever met personally any people who returned to their home country from the USA. I have met a couple of them (and I am one myself) and the tendency among them is rather to dislike America. I call it a "Pol Pot syndrome".
It's not necessarily something "very wrong" that USA did, it's just that China is catching up and the reasons for leaving the family, adjusting to a different culture and starting from close to zero in America are disappearing. This will accelerate in the future, especially when the realization that the US is a bankrupt country sinks in (heard that laughter when Geithner told Chinese students that dollar assets are safe?).
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.
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.
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.
I don't quite follow your reasoning. In order to convince you that some proof languages are readable I would need to be able to write formal proofs efficiently? Ease of writing formal proofs is not much related to readability. As I mentioned, languages that are designed to make writing the proofs easier tend to be less readable. For some examples of machine verified proofs that I consider readable you can look at the Tiddly Formal Math site (disclaimer: I am the author of that site). As for what will be formalized in someone's lifetime it's a moving target. People used to say that the prime number theorem will not be formalized in their lifetimes and many were wrong. I am happy that the proofs being mentioned in this type of argument now are much more recent. I think formalizing large areas of mathematics will advance the development of new mathematics in about the same extent as development of modern foundations of mathematics at the end of XIX century. It was not obvious to see at that time as well why there was even a need, and how it would help.
How many formal proof languages have you seen? Most of them are designed for software verification, not formalized mathematics. They are optimized to make it easier for the author, not for the reader. Vdash will (probably) use Isar which is as easy to read for a mathematician as a standard proof. There may be an excessive amount of detail that sometimes obfuscates the big picture, but there are ways to deal with that, too.
Mizar library would be an attractive target to import. It is the best library of formalized mathematics in existence. The problem is that then you would have to make Mizar the back end of the wiki, but Mizar is not free software. Writing an alternative parser for the Mizar language would be very difficult, people have tried to do that and failed. Also, there are copyright issues with trying to import the Mizar library.
Why is the plaintiff's age important enough to be mentioned in the judgment? How old one has to be to not be "young" in the eyes of the German legal system (apparently more than 33)? Is this special treatment of adult "young" people peculiar to Germany or happens in other European countries? If I am annoyed by this, does that mean I am old?
As a former mathematician I am always surprised by mathematicians who think that the natural number 4 (that is the set {0,{0},{0,{0}},{0,{0},{0,{0}}}} ) should be equal to any real number (which are usually some sets of Cauchy sequences or Dedekind sections of rational numbers).
As a high tech worker with two PhDs who is about to move back to my home country because my green card application got stuck in a 300,000 people long que at the "Backlog Elimination Center", I couldn't agree more. Of course every country has right to set its immigration policy. However, a policy that gives the preference to farm workers rather than highly educated people is clearly suboptimal in the long term.
>What am I missing here? A couple of things. For me writing software (or formalized mathematics, which is quite similar) is an expression of creativity, like writing poetry or painting. I am willing to do it without hope of ever making money on it. Another thing you are missing is the big picture of efficiency of writing software the proprietary vs. open source way. I once had to write a Windows and Linux driver for the same board that my company makes. Windows driver: 12000 lines of code. Linux driver: 200 lines patch submitted to kernel.org. How was that possible? Well, in Windows I had to implement everything from scratch. In Linux, the support for the chip was already there and I only needed to code some stuff specific to the board. Yes, it would be possible to buy some "intellectual property" for the Windows driver that would make the task easier. However, the very cost of the transaction (just the effort to find the vendor, negotiate agreement etc) would exceed the cost of effort needed for the Linux driver. I think the factor of efficiency will become more and more important as software becomes more and more sophisticated.
Here is a link to an NSA publication on the subject: Solving the Enigma
Yes, I am quite happy with my account at cosmopod.com "internet operating system" - a full remote KDE desktop delivered from UK to CA with NX protocol. It is faster to use KDE or firefox this way than locally on my 6 years old machine. There are tradeoffs related to privacy, but those may depend on the country you live in. Sometimes your data are safer when physically located in a different country than your machine at home.
Here are a couple in the past I know about not related to TopCoder:s ults.html
http://www.dtek.chalmers.se/groups/icfpcontest/re
http://icpc.baylor.edu/past/default.htm