Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Can computers be mathematicians?

quantamagazine.org

Post reply on HN
Print view View original

11–20 of 31 posts

Re: Can computers be mathematicians?

#11

Post by pirocks »

photochemsyn wrote: post #10

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 mathematic…

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.

Re: Can computers be mathematicians?

#12

Post by hutchisonc »

photochemsyn wrote: post #10

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 mathematic…

The mathlib discussed in the article does include representations of infinite cardinalities; see e.g. https://leanprover-community.github.io/mathlib_docs/data/rea.... There was also a (now completed) project to prove the independence of the continuum hypothesis from ZFC in Lean; see https://github.com/flypitch/flypitch.

Re: Can computers be mathematicians?

#13

Post by labrador »

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.

Re: Can computers be mathematicians?

#15

Post by defrost »

photochemsyn wrote: post #10

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 mathematic…

With symbolic computer algebra systems, eg:

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.

Re: Can computers be mathematicians?

#16

Post by vintermann »

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?

Re: Can computers be mathematicians?

#17

Post by lisper »

vintermann wrote: post #16

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 lig…

> 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.

You've just described category theory. ;-)

Re: Can computers be mathematicians?

#18

Post by t_mann »

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.

Re: Can computers be mathematicians?

#19

Post by Jimmy »

t_mann wrote: post #18

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 "int…

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.

Re: Can computers be mathematicians?

#20

Post by IIAOPSW »

Jimmy wrote: post #19
t_mann wrote: post #18

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 "int…

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 impa…

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.
Post reply on HN