I am just finishing up the book Math Without Numbers by Milo Beckman. This is a good book for a layperson like me, in that in introduces lots of interesting stuff and provides a kind of a map to mathematics.

I have a hunger for more knowledge about math, and I found the book a bit like an amuse-bouche before a meal that isn’t coming. I’m not entirely sure what to do about that, since I’m not prepared to return to school for math, yet I’m not satiated by superficial treatments of math from YouTube videos and the like. I think if I had taken an extra year or two of math in college, it would be easier for me to make progress on my own.

Real Numbers

I got interested in the real numbers a few years ago and read Essays on the Theory of Numbers by Dedekind, who has this amazing quote at the beginning of the book:

The present memoir soon after its appearance met with both favorable and unfavorable criticisms; indeed serious faults were charged against it. I have been unable to convince myself of the justice of these charges, and I now issue a new edition of the memoir, which for some time has been out of print, without change, adding only the following notes to the first preface.

The real numbers present a sort of confounding problem. We need real numbers to handle irrational numbers such as √2 and the like, which can be approximated. But the uncountability of the real numbers, their absolute continuity, is a property that is needed for calculus. Yet we’re unable to construct a single real number that doesn’t also belong to the set of algebraic numbers, which are countable. This is sometimes called the “hay in the haystack” problem. Neither one of us has ever seen a real number and probably never will.

Topology

Measure is an elementary topic of topology, and I’m an expert because I’m on page 35 of a book about it, Introduction to Topology. The book is great. On page 35, though, I got the answer to a question I sort of posed a number of years ago in A Heretical Calculus, why don’t we use a number system with an actual infinity and actual infinitessimals, since that’s what Newton did and for a few hundred years it seemed to be fine?

Figuring out a way to solve our problems with these “hyperreal” numbers occupied math for quite some time but the solution, the epsilon-delta definition of closeness, is not just a nice solution. It happens to open up the possibility of doing calculus to many other situations than just real numbered functions. Exercise 2.4 in Introduction to Topology has you prove that integration of functions over a fixed domain form, themselves, a metric space. This means you could in principle do anything you do with calculus over that space, like integrate.

Talking to my friend Mike Tamburro about it, I get the sense that topology is not so much about donuts and spheres and whatever as it is about questions like, what does it mean for points to be close? What is a neighborhood? What do does “connected” mean? All of these questions seem to spring forth from the idea of continuity. In our first-year calculus classes we get a very pragmatic sense of what continuity is about, but what does it really mean?

Proof

Solving the first three assignments on page 35 of the topology book, I found myself wrestling with the same old questions I have always had about proof. How do I know if a proof is complete? How do I know if a proof is good?

Many years ago my friend Tyler taught a class about theorem proving using the book Software Foundations. I wrote about this before briefly, but that class raised some other questions: if you’re not able to convince a computer of the proof, does it count as proof? What if you’re able to convince a computer but you don’t understand it yourself?

I still don’t really have the answers, but I decided the following for this attempt:

  1. I should understand that something I’m supposed to prove is true. I should understand why before attempting a proof.
  2. I should try to write a proof that would convince me, sometime in the future, when I have forgotten about this.
  3. I should not worry too much about convincing a real mathematician.

This comes down to the problem that I didn’t have to do any real proofs in college, so I never wrote proofs or had them scrutinized. Writing real proofs is probably at least half or more about having experience reading real proofs, and that isn’t something I spent much time on in college either. This is a bit like trying to write programs without reading programs.

I would say about half of my skill at programming comes from be able to read code and reading other people’s code and stealing their ideas. So to get better at writing proofs, I need to spend time reading proofs, struggling with writing proofs, and then stealing other people’s ideas when I finish them. This is all going to take time.

I would have hoped that formal proof, i.e. software proof using things like Coq and Lean would help with writing informal proofs, the kind that mathematicians like. In practice though, it doesn’t seem to be the case, because A) you might know something is true and not really be able to convince a theorem prover, because you don’t understand enough about the system or how to write the tactics or whatever, and B) it often does seem to be possible to convince the machine that something is true without really knowing what steps it took, thanks to automated tactics.

I spent some time this last week playing The Natural Number Game which is a pretty cool introduction to the Lean theorem prover. I still came away with the feeling that the game of building the proof didn’t necessarily come with a lot of understanding of what I was trying to prove. And I absolutely do not see how to take a book like Introduction to Topology and do my homework with Lean. I just have no clue how you would get started. So that remains an open question: would it be useful to learn Coq or Lean enough to be able to use it to assist with one’s homework in some other advanced class? Or is that just a bridge too far?

Lattices

I learned a little casual abstract algebra from Haskell, but one area I had never heard anything about was lattices, until I read this excellent article from Christopher Alexander called A City is Not a Tree.

Lattices are interesting for a number of reasons, but one that might surprise you is that you often do not have a total ordering between some apparently orderable items. We often want a total ordering, so that we can sort a set, but often we only have a partial ordering—some of the elements come before some of the other elements, but not every pair of elements can be compared.

Lattices turn out to be everywhere once you know about them. I was having a conversation last week about my preferences for a version control system. I’ve used (briefly) CVS, subversion, mercurial, git, Tom Lord’s arch, fossil, and darcs. I have trouble comparing some of these to each other but I have definite preferences between some of them. Because I have a favorite and a least favorite (not using version control at all), my preferences form a lattice. What makes lattices interesting is the notions of infimum (meet) and supremum (join), the idea that no matter which pair of elements you present to me, I can give you another element from the same set which is either below or above the pair you presented. When the items are directly comparable, it’s one of those two items, but if they aren’t, I can still find something else from the set to give you.

Considering my version control preferences, the join of nothing and CVS is CVS, because I would prefer you use something (anything) over nothing. The join of Tom Lord’s arch and CVS is probably git though, because I really didn’t enjoy arch when I used it and CVS has lots of well-known issues.

The book I’m reading, Introduction to Lattice Theory with Computer Science Applications uses lattice theory to solve distributed computing problems. I’m sure there are lots of other interesting applications for it. But even having a name for something causes you to search for it and notice when you have it, creating opportunities to leverage your knowledge.

Another area of abstract algebra I wish I knew more about is group theory, which apparently comes up a lot in particle physics.

Final thoughts

I think probably I will try to take a class this fall with an emphasis on proof. My feeling is that getting better at proof will make it much easier for me to explore these areas of math on my own. And being forced to do it with time constraints will probably make it flow more easily. I guess we’ll see.