Irreal

Over at Quanta magazine, Kevin Hartnett has an interesting article about using computers in the service of Mathematics. That’s nothing new, of course, but this isn’t about numerical methods or LaTeX, it’s about using computers to help develop mathematical proofs.

Even that notion isn’t new. There is, for instance, Coq, which has been doing the same sort of thing since 1989. What is new is that Mathematicians are trying to capture within another theorem prover, Lean, all known mathematics, or at least all of undergraduate mathematics. That’s a huge undertaking and they’re still only about half done. The hope is that with that knowledge, Lean will know enough to start help proving theorems.

According to the latest Mathlib Statistics, there are currently 19,305 definitions and 41,552 theorems in the system. You can, yourself, play with the system if you like. There are instructions for installing it on all of the usual operating systems or even for running it in a browser, although that will be much slower than a regular installation.

If, like many of us, you come from a Mathematical background, you’ll probably find the article interesting and may want to try the system out.

Most Irreal readers probably know the name Dijkstra, if only from his famous letter to the ACM entitled “Go To Statement Considered Harmful” and his celebrated shortest path algorithm. In fact, Edsger Wybe Dijkstra was a giant in the field of Computer Science, A Turing Award winner, and a significant contributor to both the engineering and theoretical sides of Computer Science.

Krzysztof Apt has a long and interesting biographical article about Dijkstra in Inference. Although he was an astoundingly successful academic, Dijkstra didn’t do much formal publishing. Rather, he preferred to publish much of his work in private reports that he numbered consecutively and prefixed with his initials. There were 1,318 such reports totaling over 7,700 pages. He’d typically send photocopied copies of each report to about 20 colleagues chosen depending on the report’s subject matter.

Dijkstra was interested in formal methods and in particular about writing correct programs. He thought programming should be approached like Mathematics and that every program should come with a formal proof of correctness. He was, according to Apt, a friendly and personable man but his rigidly held views could be off-putting and were often interpreted as arrogance.

Apt’s article has many interesting vignettes from Dijkstra’s life including the fact that when he married he listed his profession as Programmer on the marriage license. The Dutch authorities rejected that on the grounds that there was no such profession. Most surprising of all, perhaps, is that the famous “considered harmful” phrase did not originate with him but was from Niklaus Wirth, an editor of the ACM at the time the letter was published. Dijkstra’s original title was “A Case against the GO TO Statement.”

If you have any interested at all in the history of our field—and, really, you should—you’ll want to read Apt’s article. It full of interesting facts you didn’t know.

What could you buy for the price of a ball point pen? No much. Not a newspaper, not a cup of coffee, and certainly not a hamburger. You can get one of the ubiquitous Bic pens for a little over 11 cents if you buy a box of 60. It wasn’t always like that, of course. When they were first introduced, ball point pens sold for the equivalent \$100–\$120 in today’s dollars.

The BBC has a fascinating history of the ball point pen that discusses the early days of the ball point and how it changed writing. If you’ve ever used a fountain pen, you understand why the ball point was so revolutionary. Fountain pens leaked ink, easily smudged, had to be refilled often, and regularly left drops of ink over whatever you were writing. All of those problems went away with ball point pens.

Marcel Bich’s genius was not inventing the ball point but in mass producing it at low cost. Between 1950 and 2006, Bic sold over 100 billion of their iconic Cristal ball points.

The article says that ball point pens changed writing forever. It’s ironic, then, that another article, this time from the Atlantic in 2015, claims that the ball point pen killed cursive writing. As regular readers know, I’d consider that another benefit of ball points. The TL;DR of that article is that whereas fountain pens encourage and make easy the forming of connected letters, ball points make that harder. I’m not sure I completely buy the premise but you can read it for yourself and see what you think.