hanslub42

Thanks for the summary! This looks more doable than I thought....

On Polarhome, I used QNX, SunOS/Solaris, HP-UX, AIX and OSX. Having those running under qemu would be quite the challenge.

Until now, I have used qemu (or rather qemu-system-aarch64 in combination with binfmt-misc) on Linux to emulate e.g a Raspberry pi running on arm64. This works very well, but for e.g. Solaris or HP-UX there is the extra hurdle of getting hold of bootable media that will not freak out in the unfamiliar surroundings of a qemu virtual machine.

I have never tried, and it is possible that I overestimate the difficulty...

All the heavy lifting is done by the comments. For example: theorem dof_gt_one_inconsistent (dof : Nat) (h : dof > 1) dof ≠ 1 (in Basic.lean) is the well-known fact that any number > 1 is unequal to 1.

But the comment states: DOF > 1 implies potential inconsistency. Inconsistency of what? Lean doesn't know, or care....

This would be a good place to remember Moses Schönfinkel, who invented Combinatory Logic as a student of David Hilbert at Göttingen in 1920. His life was tragic: after his return to his native Russia he became mentally ill, and he died in Moscow in poverty. According to Wikipedia, "His papers were burned by his neighbors for heating".

In 1942, Heisenberg became the director of the Kaiser Wilhelm Institute for Theoretical Phiysics, where research into nuclear physics was conducted (on a small scale) and a Uranmaschine (small experimental reactor) was built. At that point, Heisenberg indeed didn't believe anymore in the possibility of building a fission bomb. But a year before that, Heisenberg had told Niels Bohr that he believed that such a weapon was possible. So, you're right: although there was an "atomic weapons program" in Germany, it became an "atomic energy program" quite early on, and that happened before Heisenberg became a leading figure in it. The Allies came to know this only after 1945.

There also was a "German Physics" movement that tried to discredit relativity theory and quantum mechanics as essentially Jewish. Heisenberg was called a "white Jew" in a SS periodical. The movement didn't have much success, and Heisenberg eventually became the leader of the (unsuccessful) German effort to develop an atomic bomb.

On X11:

   xsel -o -b | xsel -i -b

A humble vegetable flowering so spectacularly was bound to get the attention of H.C. Andersen, who was always interested in ugly ducklings, like himself, turning out to be beautiful and noble swans after all. From his story "Gartneren og Herskabet" ("The Gardener and the Noble Family"):

One day the gardener brought a large crystal bowl; in it floated a water-lily leaf upon which was laid a beautiful blue flower as big as a sunflower.

"The lotus of Hindustan!" exclaimed the family. [...]

"We have been looking for it in vain," they said. "We have been in the greenhouses and round about the flower garden!"

"Oh, no, it's not there," said the gardener. "It is only a common flower from the vegetable garden; but, look, isn't it beautiful! It looks like a blue cactus, and yet it is only the flower of the artichoke!"

I have in front of me a reprint of Pellegrino Artusi's famous "la Scienza in cucina e l'arte di mangiar bene" (1891). It has a recipe for "Pizza alla napoletana" (recipe #609) which is a shortcrust filled with a cream of "ricotta, sweet almonds, sugar, lemon peel or vanilla, milk", about which he comments "... a me sembra che questo riesca un dolce di gusto squisito" - a dessert of exquisite taste.

He mentions two other pizze: "Pizza a libretti" and "Pizza gravida", both of them sweet. "Our" pizza is completely absent.

It is intriguing that the above 19th century "pizza" recipe is called alla napoletana given that Wikipedia states that "... modern pizza evolved from similar flatbread dishes in Naples, Italy, in the 18th or early 19th century."