Introducing Square Harness: an open tool for mathematical research
Why we are developing an open harness for mathematical research, and how it fits into AI systems that researchers can run and control themselves.
With Louis Carillo, I have developed and made publicly available Square Harness, an open-source tool for mathematical research with language models.
Our motivation is to help build sovereign AI systems for research: systems that researchers and institutions can run and control themselves. We see three essential components in this effort: models, computing infrastructure, and a harness.
A harness is the software surrounding a model that organises how it works. A model can produce an answer to a prompt. The harness manages a sequence of steps, supplies the relevant context, connects tools when needed, and keeps track of the results. For mathematical work, this can mean producing a proof attempt, submitting it to a separate review, and returning the objections for a possible revision.
I believe that open-weight models will continue to improve and become increasingly useful for mathematical research. Their availability gives us a reason to focus on the harness: how to turn these models into tools adapted to the way mathematicians work, while retaining control over our research environment.
Square Harness is our first contribution in this direction. Its current proof workflow combines an initial attempt, a review in a separate model context, and a revision when needed, preserving the attempts and objections for inspection. We are also developing other features for research, including literature reviews, bibliographic checks, and mathematical write-ups. These remain work in progress at the time of writing.
Feel free to contact Louis or me if you would like to try Square Harness, discuss possible uses for your research, or contribute to its development.