Can computers be mathematicians?
quantamagazine.org
quantamagazine.org
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.
Advancing mathematics by guiding human intuition with AI
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).
> 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.
But 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?
Or is this more focused on letting the computer try to prove a given conjecture?
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"