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

21–30 of 112 posts

Re: A Beginning for Mathematics

#21

Post by ksd482 »

lioeters wrote: post #16
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.

That's a good point. Low level (for a lack of better term) mathematics will become extinct/saturated.

Perhaps a parallel to this is what's happening with youth sports in the US. It is becoming increasingly inaccessible.

Re: A Beginning for Mathematics

#22

Post by chneu »

waynecochran wrote: post #18

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.

Lowering the bar for the masses isn't always a good thing

Re: A Beginning for Mathematics

#23

Post by c7b »

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…

With formalized math, you only need to validate the problem statement (in theory, in practice agents have already managed to exploit Lean compiler bugs, but the incidence of those should decrease enough to be practically lusable for 'blind' validation of AI proofs in the foreseeable future).

Re: A Beginning for Mathematics

#24

Post by famouswaffles »

vld_chk wrote: post #20
robinhouston wrote: post #14

Earlier quoted context omitted.

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…

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

This is just normal though. We were building sophisticated bronze and steel tools long before any complex understanding of metallurgy or chemistry. Medicine is still the wild west.

Re: A Beginning for Mathematics

#25

Post by nilkn »

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 actually think it's the opposite: Lean proofs and autoformalization make it very easy to announce proofs alongside proofs of the correctness of those proofs (Lean certificates). It's not an absolutely fool-proof combination (the Lean kernel could still contain bugs), but it does immediately attach a very substantial degree of credibility to the result.

And that I think is essential to why some of the world's leading mathematicians are taking this so hard. In a world where we "merely" have AI systems capable of superhuman informal reasoning, verification, correctness, and acceptance could still only be conferred or anointed by human mathematicians. But a world that combines superhuman informal reasoning with superhuman autoformalization is a fundamental shakeup in the institutional order.

Re: A Beginning for Mathematics

#26

Post by jkhdigital »

> resulting in the production of an abundance of PDFs. The contents of some of those PDFs may even have important applications.

I hope, from the depths of my soul, that the static typeset report format for transmitting knowledge and understanding will finally die and be laid to rest.

Re: A Beginning for Mathematics

#27

Post by PeterWhittaker »

chneu wrote: post #22
waynecochran wrote: post #18

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.

Lowering the bar for the masses isn't always a good thing

Examples, preferably academic?

Re: A Beginning for Mathematics

#28

Post by bananaflag »

famouswaffles wrote: post #24
vld_chk wrote: post #20

Earlier quoted context omitted.

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…

>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? This is just normal though. We were building sophisticated bronze and steel tools long before any complex understanding of metallurgy or chemistry. Medicine is still the wild west.

I first wanted to say fire, even though it's a cliche, but then I thought that in antiquity we used like everything without anything that would qualify today as understanding. Also now we have a lot of stuff that we "know" it works based on complicated numerical simulation.

I think the most "understanding" we ever had was in the 40s-50s designing nuclear bombs with slide rules. It was the culture that produced the idea of psychohistory.

> Medicine is still the wild west.

Reminder that we have no idea how anesthesia works.

Re: A Beginning for Mathematics

#29

Post by Jaxan »

nilkn wrote: post #25
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 actually think it's the opposite: Lean proofs and autoformalization make it very easy to announce proofs alongside proofs of the correctness of those proofs (Lean certificates). It's not an absolutely fool-proof combination (the Lean kernel could still contain bugs), but it does immediately attach a very substantial degree of credibility to the result. And that I think is essential to why some of the world's leadin…

The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.

Re: A Beginning for Mathematics

#30

Post by Jblx2 »

waynecochran wrote: post #18

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.

Kind of makes me think of Arnold's, "On Teaching Mathematics":

https://www.maths.tcd.ie/pub/Maths/Courseware/ProblemSolving...

Post reply on HN