SAIR Foundation

A competition organised by Terence Tao and Damek Davis asked whether mathematical reasoning can be compressed into a page a language model reads before answering. Then its second stage removed the thing that made the first stage easy to fake: an answer was no longer worth anything unless it arrived with a proof a machine would check. This is what I built for both stages, and the moment that convinced me a confident answer and a correct one are completely different products.

There is a question in mathematics that has been open since the 1800s, and for one slice of it you can now attack it by search. I built a factory that produced degree-24 polynomials, submitted ten thousand scoreable pairs to a competition organised with the LMFDB and Terence Tao, and finished 54th of 256 with a score of 2.36. The interesting part is not the rank. It is that I can prove, with numbers, exactly why the score was small, and the answer says something about how these searches should be run.

A calculator multiplies two thousand-digit numbers and takes the remainder without thinking about it. Ask a neural network to do the same thing and it becomes an open research question, one that Terence Tao helped set as a competition. The answer has to be exact, because a remainder that is off by one is simply wrong. This is what I submitted to the SAIR Foundation’s Modular Arithmetic Challenge, why the obvious approach cannot work, and the one idea that made the difference.