Disclosure: I’m working with Bruno on a company around this.
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?
At which point do you think the Human mind acting as the observer of the formal mechanism will be simply exhausted by the sheer scale of complexity? Theoretically there is no upper bound but practically?
(Don't mean to insert a pessimistic note here but genuinely curious to as your no-limits optimism)
What I would really like to see is an LLM trained 19th century math checked if it can deliver the insight that propelled 20th century math, or is it just going to deliver a bunch of runabout proofs with no insight of what came next.
Disclosure: I’m working with Bruno on a company around this.
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?
> by Gödel there’s no upper bound to automation
At which point do you think the Human mind acting as the observer of the formal mechanism will be simply exhausted by the sheer scale of complexity? Theoretically there is no upper bound but practically?
(Don't mean to insert a pessimistic note here but genuinely curious to as your no-limits optimism)
What I would really like to see is an LLM trained 19th century math checked if it can deliver the insight that propelled 20th century math, or is it just going to deliver a bunch of runabout proofs with no insight of what came next.