Search for 24:07, about 3/4 down where Strogatz poses the question: "do you imagine ... there will be a time when the descendants of Lean will be able to teach themselves math, rather than having human teachers creating libraries?"
It's interesting because Kevin Buzzard in this interview basically says that other people are interested in the application of AI to proof generation, but he's not so interested in that.
But in an earlier Quanta article, he sort of said he was:
I guess the IMO work is more about having computers automatically apply known theorems and techniques to novel (but not, fundamentally, "unsolved"!) problems, while this interview alludes to the more difficult task of getting computers to solve unsolved mathematics problems, and discover proofs of interesting theorems from scratch?
Buzzard as far as I'm aware is interested in finding mistakes in mathematical work by "real" (i.e. in his own words people doing topology rather than category theory) mathematicians, so that position makes sense.
This is related to my pet favorite question of who is doing the art if an artist uses AI (e.g. [input image] <text to image AI> -> Photoshop painting/masking -> AI Upscaler -> Crop and Print to Physical Medium?
I think I feel like an artist, but part of the production of this art feels like curation, and not precisely the practice of art. The eye for composition feels similarly artistic, but the inability of envisioning the final product at the early stages (pre-AI steps) of the work is very weird, and might be the bright red line. I don’t know how I feel yet.
I have a project titled “Is This Art?” currently showing at a local coffee shop - avoiding the issue.
I have a handful of abstract urinals to remind me of exactly this perspective. It’s a very strong position on the question, as I see it. That’s a long winded way of saying: precisely, glad you mentioned Duchamp’s urinal.
I do think the answer to the question of what is art has something to do with using a human mind to create a shareable experience (incl. visual representation or tangible object). I believe the gardens at the historic plantation houses near me are art, but probably less so my neighbors dual flowerbed / produce garden. If the output of the process is entirely functional, I don’t think it’s art.
clarifying this would require more words and thoughts than I can come up with at this moment
I'm no artist but I've had an idea for a minor art project and please feel free to steal this. It's called "I pay rent therefore I am."
Basically, a neural network is set up in a public space. The artificial neurons are literally shown as Christmas lights. This neural network has a few little gadgets it can control to entertain you. Let's say, a puppet, an electronic keyboard, a pen plotter. But, the installation is not here for your entertainment. You have to pay the neural network if you want to be entertained. There's a small interface where you can make an offer, and it can either accept or counter offer, and then you can either accept or counter offer, until either one of you says "I'm walking away from this" or until there's an agreement and you insert cash. Behind the scenes, the neural network is learning how to optimize the objective function "make money", quietly figuring out which entertaining things it is good at and which are most profitable. In other words, just like us, the neural network is motivated by its need to pay rent.
Cut the artist out of the equation completely and have the artwork work for itself. If the machine has full creative control, and can even say no to you, does it have free will?
I wouldn't. I wouldn't say a human trapped in the same situation has free will either . If it could perform a variety of tasks and chooses what it performs while sustaining itself but not optimizing purely for profit and a bunch of those talk and agree to create an unemployment insurance which includes limits on self cloning i would say they have free will.
Because we can choose not to, if an AI is designed to maximize an objective it will maximize that objective. The moment we make a human with a singular objective which they pursue above all else he is no longer free either.
Optimization for one objective eliminates all degrees of freedom in a system but for different (global?) minima one of which can be picked.
But, despite all the degrees of freedom of choice, you cannot ignore the most basic objective function that nature has handed us: stay alive. You can't really choose not to buy food and pay rent.
Arguably, at least from an evolutionary perspective, all other choices and wants are in service of this objective (albeit in very indirect and abstract ways).
Disappointing that there's no mention of infinities.
How do you teach a computer to think in symbolic terms about Cantor's concepts of infinity? There's no computational representation for irrational numbers, and barely for rational numbers. Even floating-point representations are a long-standing problems - and integers? Overflows are a problem, even just signed integers are a problem.
The pencil-and-paper mathematicians and their symbolic representations of infinities, will computers and AI ever come to grasps with that?
I believe Lean handles proofs about cardinality and infinities just fine. I'm not sure what kind of computation you want to do with infinities that current computers can't? Can you elaborate? Like sure I can't represent any arbitrary real but like that's never a problem in practice. And Mathematica like software can get pretty close to representing any computable real.
I prefer not to think of AI as being separate from humans because for the foreseeable future it will be a collaboration. The divorce is a long ways off.
> theorem-proving programs that understand Lean have begun helping some of the world’s greatest mathematicians verify their work
It's exciting to think of what break throughs will occur as humans develop even more capable tools. AI's today are very advanced calculators.
You can probably train a language model to lead mathematicians on a wild goose chase for quite a while, by just proposing some definitions, proving a few trivial things about it, proposing another based on that and doing the same etc. Then you can see how long it takes for them to catch on that it's not actually going anywhere.
It seems to me older math texts in particular expect a lot of trust that there's some light at the end of the definitions tunnel. It's become more acceptable to talk (in human language) about motivations, of why we choose to go one particular path in the space of all possible constructions.
And that's the clue with math AIs too, isn't it? I'm sure they can prove endless things, but will it be things anyone cares about, unless they have carefully human-supplied motivations?
> You can probably train a language model to lead mathematicians on a wild goose chase for quite a while, by just proposing some definitions, proving a few trivial things about it, proposing another based on that and doing the same etc. Then you can see how long it takes for them to catch on that it's not actually going anywhere.
Of course one of the first things that come to mind when reading the title is first having some sort of AlphaGo-style AI go wild on collections of math proofs and then maybe some AlphaZero-style model that can get to work even without the library.
But I guess a fundamental problem for an RL-based approach (and a pretty interesting question in itself) is how difficult it would be to say what makes any mathematics "interesting".
The interview touches on the Langlands program several times, and that is a good example: how "interesting" Fargues-Fontaine curves were perceived (even by their creators) changed substantially after Peter Scholze created a whole new world for that curve to live in. So how do we tell the computer that they're sort of halfway to something really interesting, and, perhaps even more importantly, how do we communicate it to humans once we're there? Even Scholze himself was skeptical when first presented with this direction, and those are the humans most intimately familiar with those theories. Imagine how hard it would be for any human to grasp what the AI had just done, let alone judge its relevance, after it's made progress on its own, using new mathematical objects it had just developed, solving problems it had set itself. It's not like DALL-E, where anyone can just go and say - yeah, that looks like a cat with a party hat, great job.
Naturally, the first step for AI mathematics would be generating proofs of theorems that humans have already deemed interesting, rather than the AI generating entirely new research directions all by itself.
Certainly it’s an interesting problem to think about how one would formalize the notion of interesting/important mathematics. But it’s not necessary to solve that problem in order for AI to start having a big impact on how mathematics is done.
This implies that the discovery of math and the existence of math ultimately comes down to human taste and can only be learned by studying humans. I'd like to think human reasoning is a crude approximation to mathematics in all its glorious purity, not the other way around.
Big results typically have a lot of implications and connect different fields together. This sounds like something that could be measured objectively.
You can also try reproving old theorems with newly discovered methods. So if suddenly you can reprove results in different fields with a new method, that sounds like something that might be big and should be investigated by humans.
Of course, what I wrote above will miss subtle things, but there is a place for a system which can just brute force it's way through mathematics.
By formalizing the same proof system we would use to convince ourselves that this works and letting the AI the search the space of logical statements using that language
Most logical statements are uninteresting stuff like summing long sequences of integers, so now we have to sift through a heap of junk AI theorems hoping to find something interesting.
30 comments
[ 2.0 ms ] story [ 79.6 ms ] threadBut in an earlier Quanta article, he sort of said he was:
https://www.quantamagazine.org/at-the-international-mathemat...
I guess the IMO work is more about having computers automatically apply known theorems and techniques to novel (but not, fundamentally, "unsolved"!) problems, while this interview alludes to the more difficult task of getting computers to solve unsolved mathematics problems, and discover proofs of interesting theorems from scratch?
Advancing mathematics by guiding human intuition with AI
https://www.nature.com/articles/s41586-021-04086-x
I think I feel like an artist, but part of the production of this art feels like curation, and not precisely the practice of art. The eye for composition feels similarly artistic, but the inability of envisioning the final product at the early stages (pre-AI steps) of the work is very weird, and might be the bright red line. I don’t know how I feel yet.
I have a project titled “Is This Art?” currently showing at a local coffee shop - avoiding the issue.
I do think the answer to the question of what is art has something to do with using a human mind to create a shareable experience (incl. visual representation or tangible object). I believe the gardens at the historic plantation houses near me are art, but probably less so my neighbors dual flowerbed / produce garden. If the output of the process is entirely functional, I don’t think it’s art.
clarifying this would require more words and thoughts than I can come up with at this moment
Basically, a neural network is set up in a public space. The artificial neurons are literally shown as Christmas lights. This neural network has a few little gadgets it can control to entertain you. Let's say, a puppet, an electronic keyboard, a pen plotter. But, the installation is not here for your entertainment. You have to pay the neural network if you want to be entertained. There's a small interface where you can make an offer, and it can either accept or counter offer, and then you can either accept or counter offer, until either one of you says "I'm walking away from this" or until there's an agreement and you insert cash. Behind the scenes, the neural network is learning how to optimize the objective function "make money", quietly figuring out which entertaining things it is good at and which are most profitable. In other words, just like us, the neural network is motivated by its need to pay rent.
Cut the artist out of the equation completely and have the artwork work for itself. If the machine has full creative control, and can even say no to you, does it have free will?
Optimization for one objective eliminates all degrees of freedom in a system but for different (global?) minima one of which can be picked.
Arguably, at least from an evolutionary perspective, all other choices and wants are in service of this objective (albeit in very indirect and abstract ways).
https://www.quantamagazine.org/tag/the-joy-of-why/
How do you teach a computer to think in symbolic terms about Cantor's concepts of infinity? There's no computational representation for irrational numbers, and barely for rational numbers. Even floating-point representations are a long-standing problems - and integers? Overflows are a problem, even just signed integers are a problem.
The pencil-and-paper mathematicians and their symbolic representations of infinities, will computers and AI ever come to grasps with that?
i.e. https://www.bbvaopenmind.com/en/science/mathematics/georg-ca...
Magma Computer Algebra System Matrix Groups Over Infinite Fields http://magma.maths.usyd.edu.au/magma/handbook/matrix_groups_...
this dates back to the mid 1980s.
TLDR; in the same manner that humans reason about infinity: abstractly.
All the other answers have been well so i do it tongue and cheek. "With Floating Point numbers"
> theorem-proving programs that understand Lean have begun helping some of the world’s greatest mathematicians verify their work
It's exciting to think of what break throughs will occur as humans develop even more capable tools. AI's today are very advanced calculators.
It seems to me older math texts in particular expect a lot of trust that there's some light at the end of the definitions tunnel. It's become more acceptable to talk (in human language) about motivations, of why we choose to go one particular path in the space of all possible constructions.
And that's the clue with math AIs too, isn't it? I'm sure they can prove endless things, but will it be things anyone cares about, unless they have carefully human-supplied motivations?
You've just described category theory. ;-)
But I guess a fundamental problem for an RL-based approach (and a pretty interesting question in itself) is how difficult it would be to say what makes any mathematics "interesting".
The interview touches on the Langlands program several times, and that is a good example: how "interesting" Fargues-Fontaine curves were perceived (even by their creators) changed substantially after Peter Scholze created a whole new world for that curve to live in. So how do we tell the computer that they're sort of halfway to something really interesting, and, perhaps even more importantly, how do we communicate it to humans once we're there? Even Scholze himself was skeptical when first presented with this direction, and those are the humans most intimately familiar with those theories. Imagine how hard it would be for any human to grasp what the AI had just done, let alone judge its relevance, after it's made progress on its own, using new mathematical objects it had just developed, solving problems it had set itself. It's not like DALL-E, where anyone can just go and say - yeah, that looks like a cat with a party hat, great job.
Certainly it’s an interesting problem to think about how one would formalize the notion of interesting/important mathematics. But it’s not necessary to solve that problem in order for AI to start having a big impact on how mathematics is done.
You can also try reproving old theorems with newly discovered methods. So if suddenly you can reprove results in different fields with a new method, that sounds like something that might be big and should be investigated by humans.
Of course, what I wrote above will miss subtle things, but there is a place for a system which can just brute force it's way through mathematics.
Or is this more focused on letting the computer try to prove a given conjecture?