PIP News: Isabelle is Up!

Before my fall I launched a PIP (Perpetual Impossible Project).  PIPs are long-range risky undertakings that cannot be finishedPIPs contradict and subvert the very notion of tightly controlled corporate style projects: hence their manifest appeal to recusants like myself.

I won’t go into details about my particular PIP. Let’s just say it captures every delusional notion I have ever entertained. Part of my project involved installing a few Proof Assistants. Proof assistants are programs that verify formal mathematical proofs. There are many proof assistant programs available. These programs are not mathematical magic bullets. They don’t prove theorems and they don’t make the job of “theorem proving” easier. To use a programming analogy: a traditional proof is like pseudo code while a formal proof is like an assembly language program.  If you have ever written a nontrivial assembly language program you have some idea of the sheer effort required to produce a formal proof.

So, if formal proof only makes mathematics more difficult, why bother? This is like asking, so if implementing pseudo code only makes programming more difficult, why bother?

Isabelle 2011 on my Ubuntu box.

A screen shot of Isabelle 2011 on my Ubuntu machine. To install this program I had to convert a Windows machine to Ubuntu and install a host of Linux tools. Reaching this point represents a lot of water under the software bridge.

Open Source Hilbert for the Kindle

David Hilbert

David Hilbert

While searching for free Kindle books I found Project Gutenberg. Project Gutenberg offers free Kindle books but they also have something better! Would you believe \LaTeX source code for some mathematical classics.

The best book I’ve found so far is an English translation of David Hilbert’s Foundations of Geometry. Hilbert’s Foundations exposed some flaws in the ancient treatment of Euclidean geometry and recast the subject with modern axioms. Because it is relatively easy to follow, compared to Hilbert’s more recondite publications, this little book exercised disproportionate influence on 20th century mathematics. We still see its style aped, but rarely matched, in mathematics texts today.

I couldn’t resist the temptation of compiling a mathematical classic so I eagerly downloaded the source and ran it through \LaTeX.  Foundations compiled without problems and generated a nice letter-sized PDF. Letter-size is fine but I was looking for free Kindle books! I decided to invest a little energy modifying the source to produce a Kindle version. Project Gutenberg makes it clear that we are free to modify the source. Isn’t open source wonderful!

Converting Foundations was simple. The main \LaTeX file included 52 *.png illustrations with hard-coded widths in \includegraphics commands. I wrote a J script that converted all these fixed widths to relative \textwidth‘s. This lets \LaTeX automatically resize images for arbitrary page geometries. When compiled with Kindle page dimensions this fixed most of the illustrations. I had to tweak a few wragfig‘s to better typeset images surrounded by text. The result is a very readable Kindle oriented PDF version of Hilbert’s book. There are still a few problems. The Table of Contents is a plain tabular that does not wrap well and one table rolls off the right Kindle margin. Neither of these deficiencies seriously impair the readability of the text.  If these defects annoy you download the Project Gutenberg source with my modifications and build your own version.

This little experiment convinced me that providing free classic books, in source code form, is a service to mankind.  Not only does it allow you to “publish” classics on new media it also fundamentally changes your attitude toward books. Hilbert was one of the great mathematical geniuses of the 19th and 20th century. It’s hard to suppress we are not worthy moments and maintain a sharp critical eye when reading his “printed” works.  You don’t get the same vibe when reading raw \LaTeX.  Source code puts you in a, it’s just another bug infested program, frame of mind. You expect errors in code and you typically find them. This is exactly the hard-nosed attitude you need when reading mathematics.

C. K. Raju: Genius or Crank (Part 1)

Euclid's first proposition

Euclid’s first proposition

Lately I have been amusing myself by working through Euclid’s Elements. Despite studying mathematics in university, teaching it in high school and occasionally using it in my software-soaked day job I never got around to reading Euclid.

Euclid is routinely lionized as the wellspring of axiomatic mathematics. Before The Elements mathematicians were clearly out of control!  They were running around developing useful methods, (counting, fractions, roots),  and — gasp — making unjustified assertions!

Fortunately, The Elements put an end to all that and ushered in the endless age of rigorous axiomatic mathematics. I admire mathematical rigor but my tiny brain can only take so much of it before an all-pervading fog of befuddlement sets in. When I’m all fogged up there are only a few options:

  1. Reread and rework until the fog clears.
  2. Press on and review later.
  3. Give up and abase self.
  4. Take a break.

I’m a lazy S.O.B. so option (4), take a break, comes up more often than it should.  One of my favorite ways to  break away from mathematics is to read about it’s long history.  While tracing the history of The Elements I came across the writings of C. K. Raju.

C. K. Raju has written a fascinating book: (the) Cultural Foundations of Mathematics: The Nature of Mathematical Proof and the Transmission of the Calculus from India to Europe in the 16th c. CE. Raju’s book is a bit hard to get your hands on.  It’s not on Amazon but you can use World Cat to find a copy near you.

Raju’s thesis consist of these major points:

  1. Significant portions of the calculus developed in India long before Newton and Leibniz and Indian methods, particularly series expansions, came into Europe via 16th century Jesuit missionaries.
  2. European notions of rigorous mathematical proof evolved from the needs of  the Catholic Church to convert Muslims with impressive iron-clad logical arguments.  The old baffle them with bullshit tactic.  Raju claims this theological attitude worked it’s way into mathematics and resulted in the bizarre western view that deduction is superior to observation, experience and induction.
  3. The ultimate source of eastern secular knowledge, (mostly Arab and Indian), was systematically suppressed and “Hellenized” by the Catholic Church.  The church claimed  all the “good stuff” in Arab texts originated with the ancient Greeks and had been merely preserved by Arab copycats. It just wouldn’t do to credit hated, (remember the crusades),  enemies for their good ideas.
  4. Insisting on rigorous proof when teaching mathematics, especially to children, is sterile and stupid.

All of this reads like a mathematical Dan Brown novel and oddly the Catholic Church is once again the villain.  I was enjoying Raju’s account until this passage about Kepler:

Why, after all, was Tycho so secretive about his papers, not even allowing his trusted assistant Kepler to see them?  In any case, on Tycho’s sudden death, Kepler obtained not just Tycho’s observations but also the rest of his papers which contained the underlying theory. Being inclined towards heliocentrism, Kepler transformed Nilakantha’s “Tychonic” orbits to a heliocentric frame (a simple transformation). This made Nilakantha’s variable epicycles come out as ellipses. Being a professional astrologer, Kepler was good at making up stories, and he made up the story about how he had arrived at his results using Tycho’s data.

In other words Kepler is a fraud and he ripped off one of the major discoveries in astronomy, the elliptical orbits of planets, from Indian astronomers. It’s one thing to spin plausible stories about how parts of calculus may have seeped into Europe from unacknowledged sources it’s another thing to posthumously accuse someone of fraud.

What would it take to make Raju’s case?  How about some hard evidence! What about Tycho’s secret papers, do any of these documents survive and do they contain references to Nilakantha?   Now that would be a smoking gun.  Of course we don’t know of any such papers but that doesn’t mean they didn’t exist. Proof by conspiracy is a very powerful inference rule — 9/11 troofers and ufologists swear by it!  What about the claim that the transformation from Nilakantha’s variable epicycle Earth centered system to a Sun centered elliptical orbit system is “a simple transformation.”   I rather doubt it’s as simple as claimed and even if the transformation was, to use the most abused word in mathematics — trivial, it still misses the point.  The major shift was to abandon all pretense of Earth centered systems no matter how mathematically sophisticated!  Before Kepler astronomers and mathematicians, in many cultures, toyed with the idea that planets orbit the sun.  After Kepler everyone had to grow up.  Planets do orbit the sun deal with it!

And it was precisely how Newton dealt with it that made calculus something worth fighting over.  Newton’s unprecedented and monumental proof that elliptical orbits are a mathematical consequence of the inverse square law of gravity is the dividing line between modern and early science.   Nothing like it had ever been done before and even today physics and mathematics students are given to chanting we are not worthy when presented with this brilliant argument. Without Newton’s use of the calculus nobody but a few anal mathematicians would give a rat’s ass about who invented calculus.

In a later post I will argue that Raju discounts the importance of independent and coequal mathematical discovery in his account.