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

The Dark Night of Mathematics

kirwinhampshire.substack.com

Post reply on HN
Print view View original

11–20 of 321 posts

Re: The Dark Night of Mathematics

#11

Post by xg15 »

geophile wrote: post #4

> "They are forbidden from creating original works to express themselves. However, they are still permitted to comment on writing, interpret it, share their taste. They are still valued for their appraisal, presentation, understanding and appreciation of creative writing. They just can’t write creatively anymore. They can go on as an enthusiastic spectator. > ... It revealed that the process of prompting novel proofs…

My suspicion is still that this has to do with losing insight in the little specific details of the matter and general understanding.

An area where I realized that was feature engineering: Early ML systems had handcrafted features that were fed into the model. There were relatively arbitrary and the number of features you could reasonably generate that way was tiny, compared to modern systems - but it gave you some understanding what input the model got exactly and you could use it to clear up some failure modes, or be certain that the model learned something that could not possibly make sense.

Then the idea was to automate feature generation. What's not to like? Except that in practice, the automated features simply seem to become part of the blackbox and are not available anymore for understanding.

Re: The Dark Night of Mathematics

#12

Post by sibeliuss »

turtleyacht wrote: post #2

Math is having its DevOps moment. And yet, people who really understand networks are beyond valuable.

Every day I witness the crazy wonder that is network knowledge / devops + agents from my colleagues. Things that were not possible become possible, assuming deep expertise. I feel for mathematicians like the author, but it will pass once the more creative possibilities reveal themselves and the shock passes.

Re: The Dark Night of Mathematics

#13

Post by psunavy03 »

geophile wrote: post #4

> "They are forbidden from creating original works to express themselves. However, they are still permitted to comment on writing, interpret it, share their taste. They are still valued for their appraisal, presentation, understanding and appreciation of creative writing. They just can’t write creatively anymore. They can go on as an enthusiastic spectator. > ... It revealed that the process of prompting novel proofs…

As someone who has been both a software professional and a jet aviator, the same process is going to occur in both. Humans will still be in the loop, but the span of control and effectiveness of each individual human will explode. There's a reason the current plan is to augment manned aircraft with "loyal wingman" drones and smaller ones. Even in the Russo-Ukrainian War, manned aircraft are still A Thing. They've even hauled old prop trainers out of storage to put a guy in the back with an assault rifle to shoot down Shahed drones, because they're too slow for fighters.

Software is going to go through the same adaptation and exaptation process as military aviation.

Re: The Dark Night of Mathematics

#14

Post by drivebyhooting »

empath75 wrote: post #8

I spent two weeks proving a number theory result myself in lean just to see what I could do. (It’s something about composing polynomials with themselves and what other polynomials you can get that way). It was a struggle with a lot of dead ends but it is just software engineering. It’s not a world away from getting a Rust program to type check. The main problem I had with it is that LLMs will happily grind away case…

How did you learn lean? I’ve played the game but I still feel lost and bewildered. Did the action of proving with LLM assistance teach you the best?

Re: The Dark Night of Mathematics

#16

Post by discreteevent »

zemvpferreira wrote: post #10

This is what locking yourself away in an ivory tower gets you. Do things ‘for beauty’ and watch as they are automated and commoditized by the people who depend on them for their continued wellbeing, reduced to a hobby or sport. But the reduction began when you yourself started putting more importance on your enjoyment of the process over the value being provided to your customers.

> But the reduction began when you yourself started putting more importance on your enjoyment of the process over the value being provided to your customers.

Why would you make this comment? Is it envy? They were able to do things only some people can do. They enjoyed what they did and it provided value. Now the fun has been taken out of it and you seem to be saying that they deserve to have no fun? What should they have done? Prove theorems while whipping themselves in case they might have fun? Maybe it's a puritan thing? Customer value is the only value.

Re: The Dark Night of Mathematics

#17

Post by empath75 »

drivebyhooting wrote: post #14
empath75 wrote: post #8

I spent two weeks proving a number theory result myself in lean just to see what I could do. (It’s something about composing polynomials with themselves and what other polynomials you can get that way). It was a struggle with a lot of dead ends but it is just software engineering. It’s not a world away from getting a Rust program to type check. The main problem I had with it is that LLMs will happily grind away case…

How did you learn lean? I’ve played the game but I still feel lost and bewildered. Did the action of proving with LLM assistance teach you the best?

I didn’t. Claude wrote all the proofs, I just validated that it was sorry-free, didn’t have any extra axioms other than mathlib and that it proved what i wanted it to prove (there’s tools for that). I did also find a actual mathematician who did a sanity check for me.

Re: The Dark Night of Mathematics

#18

Post by 5555watch »

A silver lining to think about.. Currently there's a big issue (at least in some countries) that mathematicians must publish from 5 to 7-8 papers within a 5-year window to keep the tenure. So it's a minimum, much more is expected for grants. Yet high quality mathematical papers do take longer to finish (or sometimes to even start), especially if the researcher is working solo, not within a lab. Until today, the answer is to go for applications or for low-hanging fruit. Tomorrow, with the boost of AI help, the researchers may be able to spend more time on their "real problems"

Re: The Dark Night of Mathematics

#19

Post by robotpepi »

zemvpferreira wrote: post #10

This is what locking yourself away in an ivory tower gets you. Do things ‘for beauty’ and watch as they are automated and commoditized by the people who depend on them for their continued wellbeing, reduced to a hobby or sport. But the reduction began when you yourself started putting more importance on your enjoyment of the process over the value being provided to your customers.

Exactly! I have some many colleagues who typically say that they do "math for the beauty" while holding permanent research positions funded by the state.

Re: The Dark Night of Mathematics

#20

Post by knollimar »

discreteevent wrote: post #16
zemvpferreira wrote: post #10

This is what locking yourself away in an ivory tower gets you. Do things ‘for beauty’ and watch as they are automated and commoditized by the people who depend on them for their continued wellbeing, reduced to a hobby or sport. But the reduction began when you yourself started putting more importance on your enjoyment of the process over the value being provided to your customers.

> But the reduction began when you yourself started putting more importance on your enjoyment of the process over the value being provided to your customers. Why would you make this comment? Is it envy? They were able to do things only some people can do. They enjoyed what they did and it provided value. Now the fun has been taken out of it and you seem to be saying that they deserve to have no fun? What should they…

Don't complain that you lose funding if you sacrifice utility for a cirlejerk around craftsmanship.

I'm sure there's a programming equivalent. I believe theyre saying don't lose sight of the trees.

Post reply on HN