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?
Computational Combinatorics 