Live data from Hacker News

AI in mathematics is forcing big questions

spectrum.ieee.org

11–20 of 193 posts

Re: AI in mathematics is forcing big questions

#11
The use of computers in mathematics has been somewhat controversial from the very start.

There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understanding. I like this one quote by (allegedly) Wigner that illustrates it well:

"It is nice to know that the computer understands the problem, but I would like to understand the problem, too."

Re: AI in mathematics is forcing big questions

#13

It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very e…

I don't think you understand the workflow. Terrence Tao has done a lot of work using them in conjunction with LEAN.

You aren't having the AI check the proof, you interactively work on the same LEAN proof, handing off between the AI assistant and having LEAN check it and provide feedback for both of you when there's a mistake.

Re: AI in mathematics is forcing big questions

#14
post #11

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…

To bluntly put it in a nutshell, and state the obvious:

If you don’t understand the problem you can’t be sure that the computer does.

Re: AI in mathematics is forcing big questions

#15
post #11

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…

To bluntly put it in a nutshell, and state the obvious: If you don’t understand the problem you can’t be sure that the computer does.

Almost another layer in the peer review process in the best case right? Just a different kind of peer you have to review.

Re: AI in mathematics is forcing big questions

#17

It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very e…

AI can't yet come up with any new ideas to make the inductive leap to solve a math problem. New ideas are what get the accolades and using an old idea just means the original author missed something. We are still at the author missed something stage that AI is doing today.

It can definitely be a good research assistant though

Re: AI in mathematics is forcing big questions

#18
post #11

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…

Reminded me of this quote: the problem with machine learning is that it's the machine that does the learning

Re: AI in mathematics is forcing big questions

#19
post #11

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…

To bluntly put it in a nutshell, and state the obvious: If you don’t understand the problem you can’t be sure that the computer does.

As a programmer I definitely get annoyed when I see code and I don't understand what it does.

But I also definitely don't understand the problem if I can't get the computer to understand it, with tests.

In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof.

With all of these questions in the air, epistemology might be making a comeback.

Re: AI in mathematics is forcing big questions

#20
Human mathematicians could become “priests to oracles.”

Priests were interpreting the oracles (at least at a place like Delphi) according to the context of the people asking the questions aka participating in politics of that ancient times.

Subjectivity was a feature and I’m not sure that fits to mathematics though.

I wonder if mathematics as a science field moves more into engineering or if a different branch will emerge that is closer to that because to the point of the article, science is about understanding not just results.

Post reply on HN