One way to differentiate between an art or a craft and a science is that if a genie appeared and offered to trivialize all the discovery work of your career and simply give you the answers today, and you'd say "no", you're probably not doing science.
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.
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.
> "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 will be as auraless as ordering doordash. Watch as magic and mystery evaporate. Watch as the sun sets on our heroic age. Is there not something evil in the act of blocking all future generations of mathematicians from the experience of discovery? Forget about accuracy or even attribution. Something fundamental to the experience of mathematics is being taken."
These passages resonated with me, as someone who has been enchanted by writing software for almost 60 years. It crystalizes something that has been nagging at me for many years: I like writing software. Reviewing, testing, spec-ing, designing, etc. are all important, but they are all incidental to the actual creation of software. They are all necessary for me to do if I'm going to write software, but they are peripheral. I didn't latch on to computer programming because I got into flow state reviewing code, or spec-ing it.
And this is happening in one profession after another. For example, fighter pilots. I suspect that a fighter pilot feels about flying jet fighters the same way that I feel about programming. And he or she will soon be exactly as useless: Doing things related to flying, from the sidelines, but not doing the thing him or herself.
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.
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.
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"
> “Even if AI can prove theorems and theory-craft more efficiently than humans, and even if these proofs and theories are beautiful and interesting, and even if they are presented with elegance and clarity of thought, mathematicians will still have a place in the appraisal, presentation, understanding and appreciation of this new abundance of pleasing non-human proofs. We can still practice mathematics, learn mathematics, teach mathematics and do mathematics together.”
I am not a mathematician, but this seems like an entirely non-problematic answer to me. Mathematics is ultimately the discovery of relations and their consequences, so of course large language models were eventually going to catch up. But precisely what they do lack is ability to appreciate these relations.
The author says mathematics is a spiritual pursuit.[1] I have asked LLMs about theological topics before and they have also been able to produce perfectly cogent answers (even heavy questions like “how did Aquinas view Pseudo-Dionysius’ negation-laden description of God”). I am not the least bit shaken by this, because it is still on me to evaluate and understand, and appreciate these answers.[2] The author seems to think LLM’s pattern recognition makes redundant human understanding and appreciation, which is a logical leap that doesn’t make sense to me. Maybe the author is conflating utility and purpose? I feel bad, and hope the author takes care of themself, but I really think the author is taking a massive leap here. It is not that deep.
[1] I begrudgingly agree, but with the caveat that tending to a vegetable garden in your backyard is also a spiritual pursuit. Mathematics isn’t some special discipline that elevates you beyond other people, as much as it is useful and interesting.
[2] I of course wouldn’t consult an LLM if I actually wanted to educate myself or reason about these topics. Not only do I want to reason through them myself, but when it comes to issues in philosophy/theology/heavy stuff, you need to take in to account the perspective and experiences of the human writing them. LLMs muddle everyone’s perspective together.
The idea of ordering theorems like doordash is funny, kudos to the author for that :-)
Anyway, your "spiritual journey" doesn't matter. We'll automate mathematics because we can, because it's useful. Don't like it? Well, should have not chosen a capitalist economic system that rewards scientific progress so much.
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.
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 checking in Lean until the end of time and it’s up to you to see patterns and find dead ends. For example it wasn’t until I suggested to try translating the problem to a different characteristic that Mythos one shotted the proof (and found a counterexample for a related question I was working on).
My main problem now is _what to do with it_. I am not an academic, don’t know any academics and it’s a minor problem that I picked because I thought it was tractable and turned out to not be in the literature and fairly complicated, and the only reason I spent as much time on it as I did is that I thought I was an hour away from cracking it for about 10 of those days.
(In case anybody is curious about the proof, it’s that you can’t compose a single two variable polynomial over the integers with itself and any number of integer constants via substitution to generate all polynomials, but you can with x^2 - y and 1/2 if you allow rational numbers)
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.
Pretty sure software developers already had that moment with coding agents. They can't really admit it like this, as it affects their employability now.
One way to differentiate between an art or a craft and a science is that if a genie appeared and offered to trivialize all the discovery work of your career and simply give you the answers today, and you'd say "no", you're probably not doing science.
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.
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.
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.
> "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 will be as auraless as ordering doordash. Watch as magic and mystery evaporate. Watch as the sun sets on our heroic age. Is there not something evil in the act of blocking all future generations of mathematicians from the experience of discovery? Forget about accuracy or even attribution. Something fundamental to the experience of mathematics is being taken."
These passages resonated with me, as someone who has been enchanted by writing software for almost 60 years. It crystalizes something that has been nagging at me for many years: I like writing software. Reviewing, testing, spec-ing, designing, etc. are all important, but they are all incidental to the actual creation of software. They are all necessary for me to do if I'm going to write software, but they are peripheral. I didn't latch on to computer programming because I got into flow state reviewing code, or spec-ing it.
And this is happening in one profession after another. For example, fighter pilots. I suspect that a fighter pilot feels about flying jet fighters the same way that I feel about programming. And he or she will soon be exactly as useless: Doing things related to flying, from the sidelines, but not doing the thing him or herself.
AI is stealing all the fun parts.
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.
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.
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"
> “Even if AI can prove theorems and theory-craft more efficiently than humans, and even if these proofs and theories are beautiful and interesting, and even if they are presented with elegance and clarity of thought, mathematicians will still have a place in the appraisal, presentation, understanding and appreciation of this new abundance of pleasing non-human proofs. We can still practice mathematics, learn mathematics, teach mathematics and do mathematics together.”
I am not a mathematician, but this seems like an entirely non-problematic answer to me. Mathematics is ultimately the discovery of relations and their consequences, so of course large language models were eventually going to catch up. But precisely what they do lack is ability to appreciate these relations.
The author says mathematics is a spiritual pursuit.[1] I have asked LLMs about theological topics before and they have also been able to produce perfectly cogent answers (even heavy questions like “how did Aquinas view Pseudo-Dionysius’ negation-laden description of God”). I am not the least bit shaken by this, because it is still on me to evaluate and understand, and appreciate these answers.[2] The author seems to think LLM’s pattern recognition makes redundant human understanding and appreciation, which is a logical leap that doesn’t make sense to me. Maybe the author is conflating utility and purpose? I feel bad, and hope the author takes care of themself, but I really think the author is taking a massive leap here. It is not that deep.
[1] I begrudgingly agree, but with the caveat that tending to a vegetable garden in your backyard is also a spiritual pursuit. Mathematics isn’t some special discipline that elevates you beyond other people, as much as it is useful and interesting.
[2] I of course wouldn’t consult an LLM if I actually wanted to educate myself or reason about these topics. Not only do I want to reason through them myself, but when it comes to issues in philosophy/theology/heavy stuff, you need to take in to account the perspective and experiences of the human writing them. LLMs muddle everyone’s perspective together.
Well for me the twilight had already come when I realized I’d never amount to a decent mathematician. Maybe this is rather a common experience?
LLMs just democratized that process.
The idea of ordering theorems like doordash is funny, kudos to the author for that :-)
Anyway, your "spiritual journey" doesn't matter. We'll automate mathematics because we can, because it's useful. Don't like it? Well, should have not chosen a capitalist economic system that rewards scientific progress so much.
Math is having its DevOps moment. And yet, people who really understand networks are beyond valuable.
So true. Add me on LinkedIn?
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.
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 checking in Lean until the end of time and it’s up to you to see patterns and find dead ends. For example it wasn’t until I suggested to try translating the problem to a different characteristic that Mythos one shotted the proof (and found a counterexample for a related question I was working on).
My main problem now is _what to do with it_. I am not an academic, don’t know any academics and it’s a minor problem that I picked because I thought it was tractable and turned out to not be in the literature and fairly complicated, and the only reason I spent as much time on it as I did is that I thought I was an hour away from cracking it for about 10 of those days.
(In case anybody is curious about the proof, it’s that you can’t compose a single two variable polynomial over the integers with itself and any number of integer constants via substitution to generate all polynomials, but you can with x^2 - y and 1/2 if you allow rational numbers)
I just cleaned out the gutters on my house. Took a while to direct the guys I hired, but feel pretty proud of the result.
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.
Pretty sure software developers already had that moment with coding agents. They can't really admit it like this, as it affects their employability now.
He sounds as someone really pedantic who never understood what math is about or why it is important.