Gowers chose good old-fashioned AI in 2022
Tracing back to Gowers’ 2022 job opening:
In brief, the approach taken will be what is often referred to as a GOFAI approach, where GOFAI stands for “good old-fashioned artificial intelligence”. Roughly speaking, the GOFAI approach to artificial intelligence is to try to understand as well as possible how humans achieve a particular task, and eventually reach a level of understanding that enables one to program a computer to do the same.
Some context here: back then ChatGPT hadn’t taken the world by storm yet, let alone anyone seriously considering applying LLMs to crack mathematics.1
Even so, some of the crowd on Hacker News seemed to be disappointed that he chose to attack it using GOFAI:
This is the opposite direction to what I expected to see for new theorem proving efforts: “Good old fashioned AI” vs leveraging advances of deep learning for natural language. [dzdt]
It sounds as if the author is not well informed about the recent advancements and findings from the literature and research community on deep learning. […] it currently looks like if just scaling up further probably solves them all. [albertzeyer]
I’d be really hesitant to be a PhD student in the GOFAI or natural language datamining approaches since I think this could easily be solved by ML in the next five or ten years by ML (specifically at least one well known unsolved research problem being solved by AI). I hope that I’m wrong… I like math as a human endeavor. [tgb]
These people seem to be right, now that OpenAI has claimed a solution to a Millennium Prize Problem, four years and four months later.
But Gowers isn’t wrong either, knowing how the math community reacted to that (Mathematicians aren’t mourning their craft): approaches like that weren’t very interesting to mathematicians. He had already said in the job opening who he was looking for:
[…] if you are not fully satisfied with a proof unless you can see why it was natural for somebody to think of it, then that is better still.
I would expect a significant proportion of people reading the document to have an instinctive reaction that the way I propose to attack the problems is not the best way, and that surely one should use some other technique — machine learning, large search, […] — instead. If that is your reaction, then the project probably isn’t a good fit for you, as the GOFAI approach is what it is all about.
[…] even a program that could solve only fairly easy problems but in a sufficiently human way that it could explain how it came up with its proofs could be a very valuable educational tool.
In the aftermath, or should I say after math, we truly understand why he’s interested in that in the first place: the whole point is really understanding. Gowers’ kind of AI comes with understanding, or you might say meta-understanding: he would understand how humans come up with proofs so well that he’s able to automate proving. Robotone, his earlier program with Mohan Ganesalingam, is one example: it mechanically finds proofs of simple problems and writes them up in a way that is hard to tell from a human’s (Ganesalingam and Gowers 2017). Explaining how it came up with them is what the 2022 project set out to add.
The declarations are basically saying the same: they don’t care who gets the answer first. Getting the understanding first is more important. In the Fields medallists’ words,
solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight.2
In that sense, Gowers’ GOFAI hasn’t lost yet.
References
Footnotes
Not quite no one: OpenAI’s GPT-f was already proving theorems in Metamath in 2020 (Polu and Sutskever 2020), and one of the commenters below suggests GPT-3. But that was a long way from research mathematics.↩︎
Gowers himself didn’t sign it, because of this very sentence. See A flood from within the community.↩︎