Yesterday, the inaugaration of Joe Biden as President, brought a feeling of relief and hope, despite my general pessimissm about the longterm survival of America. Yes, now we have a man in the office (rather than a parody of a man), but tens of millions prefer a parody of a man, identify with lack of integrity, morality or intelligence (I was appalled to see one supporter of the exiting clown prince yell, "He is one of us"). China is correct to control social media. When you have a population of largely emotion-driven humans without much in the way of higher principle or intelligence, it is madness to connect them instantly to one another and amplify every metaphorical emission of the gas of decay.  Competing (in the race to destruction) we have the grotesque perverts (I do not mean sexually, since adult consensual sex is strictly the business of the participants) who infected our universities from the 1960's onward apparently preaching that white, Christian, Western Civilization should apologize for its achievements and open the gates to every barbarian horde that demands a more pleasant place to live. Yes, America began with people leaving Great Britain seeking a better life, but they went to an unsettled, wild land and tamed it, displacing the sparse population of natives, but that has always been the way of evolution--until now where the superior group is being taught to move aside voluntarily for that which could normally not compete.

It could have been so different. America would welcome applicants for citizenship who offered something and who did not overwhelm the present capability to bring in more population. The days of trying to populate a wilderness are long passed. There are too many people here now (and everywhere on Earth for that matter). It is a zero sum game, but that is not the worst of it. Already we begin to see infrastructure failures, more power failures, etc. as the marginally competent are given jobs. NASA can no longer field its own hardware, but hey, they have a diverse workforce. The national lab system, along with the US military, actually employs foreign nationals. I wonder if I am living in a madhouse where the inmates have taken over.

Well, if the essential goodness of a single man in a single office can overcome all of the above, then President Biden has a chance. I think of Lot trying to find smaller and smaller groups of good men...

I am old and tired, but persist in my research and writing. I published my best work in neutrino physics, Solar neutrino parameters and then returned to formal mathematics, resuming work with the automated proof assistant, Isabelle. I am in the process of writing a tutorial on using Isabelle for classic mathematics, proving that the square root of a prime number (the problem was originally that of the Pythagoreans, i.e., how to deal with the diagonal in a unit square, which turns out to be an incommensurable number) cannot be a rational number. There are many ways to go on that. I am following one of the routes taken by the Isabelle community, where the square root of two is assumed to be rational and then a contradiction is proven, i.e., that p must divide both m and n of the ratio square root of p = m/n with m and n positive integers n non-zero and coprime, but p is prime so cannot be 1 yet gcd(m,n) must be 1 if they are relatively prime.

I was a little unhappy to see Isabelle using properties of real numbers in the proof, which is required apparently because abstract properties involving division demand a field and the integers cannot be a field since they do not have a multiplicative inverse. Isabelle does take the approach of deriving most properties of numbers from basic principles, e.g., the Peano axioms, rather than stating axioms or postulates. In that way, they build a rock-solid structure that rests upon formally proven natural deduction steps and continues in the same manner.

...and so it goes, recalling one of my late wife's (Cheri) common utterances.