In the past few weeks, AI labs have reported solving long-standing problems, including OpenAI’s claimed Navier–Stokes proof. Mathematicians fear for their jobs, and others hope math education will finally become unnecessary.
Bruno Buchberger, who invented Gröbner bases in 1965, gave his answer in the inaugural lecture of ACM SIGSAM. There will be no “math winter”: mathematics has always aimed to trivialize itself, and by Gödel there’s no upper bound to automation, so human genius just moves up a level.
He’s also done this before. In 2002 his Theorema system re-invented the Gröbner bases algorithm automatically from the bare specification, by analyzing failed correctness proofs. That’s proof generation, not proof checking. He argues logic + LLMs should beat Lean + LLMs with far less compute. Terrence Tao’s latest video ends with a strikingly similar proposal a few days later.
Given the surge of interest, he’s resuming Theorema and founding a company around it.
Is logical synthesis the next layer, or will “LLM + Lean + compute” win anyway?