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

A Beginning for Mathematics

daniellitt.com

Post reply on HN
Print view View original

11–20 of 112 posts

Re: A Beginning for Mathematics

#11

Post by vld_chk »

I am not a mathematician, but I can’t see how we are going to address the problem which we already see in coding:

Impossibility to independently validate all AI results

And in math it goes even worse. In coding code reviews are typically still the form of action you do within days. In math, historically, the lifecycle of proof is months if not years. Take as an example Millennium problems. They require at least two years of validity after publishing. Two years! In modern times with amount of output AI can produce, it feels like infinity.

We are inches close if not at the moment already when humans can’t reliable validate proofs and mathematics produced by AI. Then next research will be based on this AI-written-no-human-in-the-loop results. And we will end up in just few years in a world where novel and frontier problems will be articulated by AI and proven by AI based on AI results and humans will be incapable of understating the mere nature of the solution.

Re: A Beginning for Mathematics

#12

Post by esafak »

> I think so. This machine might produce answers we value, but it would not, in itself, produce human understanding of those answers.

It's nice that the author is optimistic, but won't the AI be best placed to dumb down its increasingly complex proofs into a language us lowly humans can understand? To keep thinking until it can refactor complex proofs into ones from 'the book'?

Re: A Beginning for Mathematics

#13

Post by Bluestein »

I love how this is (without slighting the problems entailed) coming at it from a perspective of infinitude and abundance (we will always have more problems to solve) - which is the correct framing, particularly when dealing with ideas, or fields in the which ideas are the driver/product/output/material, and ideas themselves, the field itself, are infinite.-

PS. The validation problem, being one.-

Re: A Beginning for Mathematics

#14

Post by robinhouston »

vld_chk wrote: post #11

I am not a mathematician, but I can’t see how we are going to address the problem which we already see in coding: Impossibility to independently validate all AI results And in math it goes even worse. In coding code reviews are typically still the form of action you do within days. In math, historically, the lifecycle of proof is months if not years. Take as an example Millennium problems. They require at least two y…

I don't think that's actually the real problem. Along with the progress in answering mathematical questions, recent progress on AI-powered autoformalisation has been astonishing. All the recent AI discoveries have been accompanied by Lean proofs.

And, yes: that doesn't absolutely guarantee correctness. The Lean kernel has had soundness bugs, and may have some still. But it's pretty strong evidence of correctness nevertheless.

The concern among mathematicians is not mainly that they doubt the correctness of any of these discoveries, but that human understanding may be devalued.

Re: A Beginning for Mathematics

#15

Post by magicalist »

esafak wrote: post #12

> I think so. This machine might produce answers we value, but it would not, in itself, produce human understanding of those answers. It's nice that the author is optimistic, but won't the AI be best placed to dumb down its increasingly complex proofs into a language us lowly humans can understand? To keep thinking until it can refactor complex proofs into ones from 'the book'?

As they go on to explain, a human understandable proof is different than a human actually understanding the proof. That actual human understanding (like, in a brain of a human) is one of their stated goals.

Producing human understandable proofs is possibly a job best for humans today, but the author appears to agree with you that this is probably fleeting (and argues that even if you disagree, it should probably be treated as if it is fleeting when planning for the future):

> Right now AI systems arguably underperform us at theory-building, asking questions, exposition, … so we could prioritize and reward those skills. I think this is unwise: compare the speed at which the academy adapts to the speed at which model capabilities improve. We need to consider the endgame. If the models remain incapable in some domain, we can adjust later.

Re: A Beginning for Mathematics

#16

Post by lioeters »

ksd482 wrote: post #2

> I propose the following reconceptualization of the goal of a mathematics PhD: to become a world expert on some interesting, deep topic, and to be able to convey that interest and understanding to others. Part of operationalizing this might be a thesis, but the degree would be awarded primarily on the basis of a rigorous defense, in which the student explains the topic to their examiners until they are satisfied. I…

Another bottleneck is money required to pay corporations who own the technology to "do mathematics". In that future, there will never be another Ramajunan.

Re: A Beginning for Mathematics

#17

Post by ninalanyon »

ksd482 wrote: post #2

> I propose the following reconceptualization of the goal of a mathematics PhD: to become a world expert on some interesting, deep topic, and to be able to convey that interest and understanding to others. Part of operationalizing this might be a thesis, but the degree would be awarded primarily on the basis of a rigorous defense, in which the student explains the topic to their examiners until they are satisfied. I…

> a refreshingly forward looking idea

What?

"a rigorous defense, in which the student explains the topic to their examiners until they are satisfied."

is exactly how PhDs were awarded for hundreds of years.

Even my BSc in Applied Physics (1977) had a viva voce that was a substantial fraction of the final exam.

Re: A Beginning for Mathematics

#18

Post by waynecochran »

As someone who has a degree in math, I still can't help but think mathematicians are getting a little bit of a comeuppance. In a lot of areas of mathematics there had been little effort to make the work understandable and leaves numerous folks who could benefit from the knowledge on the outside looking in. Now AI comes along and do the same to mathematicians. Makes me chuckle a little bit.

Re: A Beginning for Mathematics

#19

Post by kenjackson »

vld_chk wrote: post #11

I am not a mathematician, but I can’t see how we are going to address the problem which we already see in coding: Impossibility to independently validate all AI results And in math it goes even worse. In coding code reviews are typically still the form of action you do within days. In math, historically, the lifecycle of proof is months if not years. Take as an example Millennium problems. They require at least two y…

But one of the things AI also excels in is summarizing and can do so hierarchically. One of my favorite things to do with a concept I'm new at is "ELI5" then "explain like I'm a high school student" then "explain like a bright undergrad in XYZ" then "explain to a working professional in this domain". It's a lot of steps, but I've found it very effective (for me) to learn with -- and I've done something similar with code and math (although not math proofs -- I'm not a mathematician). But my point is that I think we can use AI to also teach us these proofs they're building in a way that I don't understand today about human proofs.

If we use AI well here we could actually understand math much better than we do now.

Re: A Beginning for Mathematics

#20

Post by vld_chk »

robinhouston wrote: post #14
vld_chk wrote: post #11

I am not a mathematician, but I can’t see how we are going to address the problem which we already see in coding: Impossibility to independently validate all AI results And in math it goes even worse. In coding code reviews are typically still the form of action you do within days. In math, historically, the lifecycle of proof is months if not years. Take as an example Millennium problems. They require at least two y…

I don't think that's actually the real problem. Along with the progress in answering mathematical questions, recent progress on AI-powered autoformalisation has been astonishing. All the recent AI discoveries have been accompanied by Lean proofs. And, yes: that doesn't absolutely guarantee correctness. The Lean kernel has had soundness bugs, and may have some still. But it's pretty strong evidence of correctness neve…

I am not that worried, but rather just observing. Humanity is about to enter the phase when we will be using things based on ideas no human ever properly understands. This thought … disturbing, somehow?

It is perfectly valid counterpoint to say that we already do it. We everyday use myriad of things, tools, and software we have 0 clue how it operates. But for us as humans it was reassuring that we know that at least there are a few other alive humans who know it, who create it and who can explain it.

With AI soon that comforting zone will be gone.

Post reply on HN