Announcing the Small Numbers Project

Hello! It’s been a while. I’ve been busy at my new job writing software, and recently I got the itch to do some math again. Of course, I don’t have time to think deeply about proofs and theorems, but I do have time to write some fun algorithms. I found a new outlet for me to stay connected to the math community while still primarily writing code: the Small Numbers Project.

This week, my company had a hackathon where we could essentially have a few days to build whatever we want. I spent my hackathon building algorithms to compute van der Waerden numbers and Szemerédi numbers. I also included script to generate constraint systems that verify the Erdős Discrepancy Problem for C=1 and C=2. There are a lot more things we could do here, such as summarizing results in Ramsey numbers, anti-van der Waerden numbers, etc.

There are two approaches in the current code: Z3 SMT systems and backtrack search. The SMT systems are probably a good start if you’re less familiar with C code, which I used for the backtrack search algorithms. Running SAT solvers and theorem provers is probably easier to do than to compile and run the custom tools I built. However, this is an example of an area where custom algorithms are faster: simple backtrack algorithms (with a little bit of care in pruning the search tree) out-perform the general theorem provers in almost all cases.

The one case where Z3 is probably much better than backtracking is the Erdős Discrepancy Problem. I became aware of this problem after Konev and Lisitsa used a SAT solver to prove the C=2 case at N=1161. The proof their solver output was a staggering 13 GB! After this came out, I worked with an undergraduate student, Daniel Geiselhart, to reproduce their result using the same SAT formulation, but with Z3 instead. Daniel found that the Z3 proof was much smaller! We didn’t end up doing anything with that proof, but I decided to reproduce our work here. The Z3 scripts are included, but I haven’t had time to run the scripts on a machine with enough memory (8 GB does not appear to be enough). Perhaps you will have better luck!

Please contribute to the project! There are a lot of things that can be added to the project, including summaries of existing work, better descriptions of known numbers, and – most importantly – new numbers! Ramsey numbers are notably missing from the project, but only because the symmetry involved requires a lot more code than working on the integers. Please add an issue if you have more ideas. Fork the repo and open a pull request with new content.

Where do you think this project can go?

So Long, and Thanks for All the Theorems

Since I first learned about graph theory in my intro algorithms class, I have been intensely focused towards learning more about graphs and doing mathematics as a passion and a profession. At the end of this semester, I close the book on that part of my career, leave my academic position, and return to my original plan: developing software.

The Erdős Discrepancy Problem

Computational combinatorics made a big splash last spring when Konev and Lisista announced their SAT-solver-based proof of the Erdős Discrepancy Problem for constant . Recently, Le Bras, Gomes, and Selman announced another SAT-based solution for , but when restricting the sequences to have a special property.

I was working on a draft blog post to talk about these results, but then Terry Tao went and solved the full conjecture. I tweeted about it and got many responses, my favorite being simply the following image:

To help those who have difficulty with Tao’s paper (and I am not qualified to read any part of his solution), I made a short video describing the problem, or read below.

Hypohamiltonian Planar Graphs

Brendan McKay uploaded a short-but-sweet article to the arXiv titled Hypohamiltonian planar cubic graphs with girth five. Let’s quickly break down all of the words of this title:

1. A graph is hypohamiltonian if it does not contain a hamilton cycle, but the deletion of any vertex does create a hamilton cycle.
2. A planar graph is a graph that can be embedded in the plane with no edge crossings.
3. A cubic graph is a 3-regular graph.
4. The girth of a graph is the length of the shortest cycle.

McKay details the search for the smallest (and first known) graphs of this type, which have order 76. There are three non-isomorphic examples. The data for these graphs (and more) is available online [Note: at this time, it appears the data is not yet online].

The three smallest examples of hypohamiltonian planar cubic graphs of girth 5. The numbers give the face lengths for faces other than 5-faces. Figures by B.D. McKay.

Happy Birthday, Joan Hutchinson!

Bernard Lidický and I organized an AMS Special Session on Extremal and Structural Graph Theory last weekend. It was a wonderful session, filled with wonderful speakers talking about some amazing mathematics.

Notably missing was Joan Hutchinson, who we invited but she declined because she was celebrating a milestone birthday on Sunday. That’s a very good reason to miss the session, and we missed her greatly. However, we did want to share our well-wishes.

Thanks to all who helped with the session and the making of this video! A few participants were missing at the time of filming, but you can try finding your favorite graph theorists in the (very short) video above.

Shannon Capacity of Odd Cycles

Breaking news: Mathew and Östergård have improved lower bounds on the Shannon capacity of some odd cycles. These improvements over a very old and difficult problem come via some sophisticated algorithms.

Announcement: Computational Combinatorics at CanaDAM

A quick announcement to those who may be interested. Jan Goedgebeur, who has done many nice things including the wonderful House of Graphs, is organizing a Minisymposium at CanaDAM this summer. The minisymposium is Algorithmic Construction of Combinatorial Objects and will be on June 2, after Brendan McKay’s plenary talk (regular readers will remember him from several topics). See the CanaDAM 2015 page for more details about the larger conference. Unfortunately, I cannot attend, as I will be busy at that time.

GRWC 2015 Announcement

We take a small break from our usual discussions in order to announce that applications for GRWC 2015 are now online! See the announcement below.

On the arXiv

Whenever I write a paper, I put it on the arXiv. The arXiv is an open-access paper repository run by Cornell University. It’s pretty fantastic to know that almost anyone can have an immediate international audience by posting a paper to the arXiv. My use is two-fold: I upload papers and I look forward to the evening paper dump in my RSS feed five times a week. It is a great way to be actively connected to the research world. As such, I try to convince my coauthors to upload papers to the arXiv and have never had one complaint.

That is, until something interesting happened. I’ll tell the story very quickly, then talk about pros and cons for using the arXiv. This will entirely skip any copyright issues with journals, and focus on the benefits of public/private preprints. Please add your comments!

Boron and Buckyballs

Recent news from the world of chemistry: the result is really the experimental observation of a special new molecule. People call it a “Boron Buckyball”, but this irritates me since we know that the buckyball is a specific fullerene on 60 vertices. In particular, it is the smallest fullerene that satisfies the independent pentagon rule. This new Boron molecule is called “Borospherene” and is quite interesting in its own right, as seen below:

The borospherene molecule. Credit: Zhai et al.

The structure is very interesting when you consider it as a spherically-embedded (i.e. planar) graph: there are many triangular faces which create a cube-like structure, two of the faces of this cube are 6-faces, and the other four are 7-faces! These interesting heptagonal structures are particularly interesting. In the figure above, it appears to be a unit-distance embedding, and this creates a rotation in the opposing 6-faces.

Let’s dig more into the structure of this object, but also into the computational part of the experiment.