8 ms·

What does the end of mathematics look like?

A_D_E_P_T 1y ago
We'll know that the time draws nearer when an AI confirms or refutes Mochizuki's proof of the abc conjecture. As of right now, I don't think they're capable of doing that. And, as they can't even check a very (very!) complex proof, they won't be able to conjure any inhumanly complex proofs de novo. Also: > To expand: what if the practice of mathematics becomes completely determined by the diktats of a vast capitalist machinery of proprietary machine learning models churning out proof after proof, and theory after theory, conjured from the aether of all possible true statements? I don't think that this is possible even in theory, as computational resources are limited and "the aether of all possible true statements" is incomprehensively vast. (There's a massive orders-of-magnitude difference in size between true-seeming-yet-false statements and the number of elementary particles in the visible universe. More statements than particles.) You can't brute force it.
- bryanrasmussen 1y ago
  also why would capitalists expand resources on churning out proof after proof when mathematical proofs are not patentable?
  - auggierose 1y ago
    That will change quickly if capitalists see that as an obstacle. Right now, they don't really care about that, as for example software (much of which is just math) is already patentable in the US.
  - awanderingmind 1y ago
    A reasonable question - another way of looking at it is that theorems are just a side effect of mathematical research. Much of the world economy depends on things like cryptography, which involves a bunch of theorems. The question is then 'what as yet undiscovered mathematical realms might models think up that could make people money'? It is hard to imagine what doesn't exist yet, but much harder to imagine that all potentially profitable mathematics has already been discovered. This could 'just' look like algorithmic improvements.
- andyjohnson0 1y ago
  > We'll know that the time draws nearer when an AI confirms or refutes Mochizuki's proof of the abc conjecture. As of right now, I don't think they're capable of doing that. And, as they can't even check a very (very!) complex proof, they won't be able to conjure any inhumanly complex proofs de novo. I agree, but... Spend time formalising a large part of existing mathematics and proofs, train a bunch of sufficiently powerful and generative models with that, and with cooperative problem solving and proof strategies, and give them access to proof assistants and adequate compute resources, and something interesting could happen. I suspect the barrier is finding a business model that would pay for this. Turning mathematics into an industrial, extruded-on-demand product might work, but I dont know who (except maybe the NSA) would stump-up the money.
- n4r9 1y ago
  Why would an AI confirmation or rejection be more convincing than the proof itself?
  - esperent 1y ago
    Rejection: an incredibly complex proof can fall for (comparatively) simple reasons. If the AI scans the entire proof and says yep, there's the flaw, page 126 theorem X contradicts <well established known theorem> then a human can verify this without having to understand the whole proof. This could lead to the proof being rejected entirely, or fixed and strengthened. Confirmation: if the AI understands it well enough that we're even considering asking it to confirm the proof, then you can do all kinds of things. You can ask it to simplify the entire proof to make it easier for humans to verify. You can ask it questions about parts of the proof you don't understand. You can ask it if there's any interesting corollaries or applications in other fields. Maybe you can even ask it to rewrite the whole thing in LEAN (although, like the author, I know nothing about LEAN and have no idea if this would be useful).
  - zarzavat 1y ago
    Presumably an AI would formalise the proof in a system such as Lean, then you only need to trust the kernel of that proof system. Rejecting a proof would be more complicated, because while for confirming a proof you only need to check that the main statement in the formalisation matches that of the conjecture, showing that a proof has been rejected requires knowledge of the proof itself (in general).
    - lblume 1y ago
      > requires knowledge of the proof itself (in general) Why? If a proof is wrong it has to be locally invalid, i.e. draw some inference which is invalid according to rules of logic. Of course the antecedent could have been defined pages earlier, but in and of itself the error must be local, right?
      - IsTom 1y ago
        Human-written proofs are not written in Lean to be checked easily and there'll be potentially many formalizations for written prose and only some of them will be what the author intended. You need to pick the right formalization before you can say that this proof has local errors.
- awanderingmind 1y ago
  I am not suggesting models will be capable of generating 'all' proofs - that is clearly impossible. Merely that they will get better at doing so, and there is no clear reason at the moment to believe they will never reach a human level of competence. If you have one model functioning at such a level, it is presumably trivial to have a million of them, none of which will need to be paid, housed, or sleep etc.
hliyan 1y ago
Considering that mathematics is, at its core, a language for defining relationships between quantities, and then relationships between those relationships, so on and so forth, I think it's fair to assume that the possible number of such relationships are infinite. Some of these relationships will obviously be useful in the real world, but they don't always have to be. I too, suspect that we can keep on building theorems on top of theorems with increasing complexity, until a point is reached that it becomes just too tedious (but not impossible) for a human being to work through the proof.
- camjw 1y ago
  > a language for defining relationships between quantities Could you expand on this? I don't see maths as a language for quantities specifically (i.e. what does symmetry have to do with quantities). > just too tedious (but not impossible) for a human being to work through the proof. Already happened with the four colour theorem arguably.
- initramfs2 1y ago
  just the zfc axioms alone are already infinite. It's an axiom schema ranging over an infinite number of actual statements. That's just statements, without even considering symbols as you're saying.
  - bananaflag 1y ago
    Well you can just put the nbg instead, which is finitely axiomatizable
- Someone 1y ago
  > I think it's fair to assume that the possible number of such relationships are infinite That’s easily proven to be true. “Two plus two equals four” is a theorem, so is “three plus three equals six”, etc.
  - im3w1l 1y ago
    Well I think the question should be how many interesting relationships there are.
N2yhWNXQN3k9 1y ago
This article is written in an unnecessarily extravagant style, IMO. Also, I appreciate anonymity, but, to my point > I live by myself in a remote mountain cave beyond the ken of civilised persons, and can only be contacted during a full moon, using certain arcane rites that are too horrible to speak of. Okay.
- xdfgh1112 1y ago
  Agreed if I had saw that first I wouldn't have clicked
- BSDobelix 1y ago
  >>I live by myself in a remote mountain cave = I live in California, and the nearest Starbucks is more than 20 miles away. >>can only be contacted during a full moon = As a night person, I am awake when the streetlight outside my house turns on. >>certain arcane rites that are too horrible to speak of = In order to contact me, you must install Microsoft Teams. Overall, it's not that bad, except for the MS team thing. ;)
  - bubblyworld 1y ago
    The man is south african, we are geologically blessed and have a lot of pleasant remote mountain caves =)
    - BSDobelix 1y ago
      Okay, I will revert everything. The cave, the moon, and the rituals are all real. It's impressive how much reality is based on location :-)
      - bubblyworld 1y ago
        That's the spirit!
    - awanderingmind 1y ago
      True! I don't literally live in a cave, but fortunately not everyone is so allergic to whimsical language :D.
hackable_sand 1y ago
When does math become recreational for people?
- coolcase 1y ago
  At a young age?
- srean 1y ago
  When you do it with love
- awanderingmind 1y ago
  In my case, when you aren't paid to do it, and don't have (much) time to study it formally anymore.
- plopilop 1y ago
  How is that any different than people programming for fun?
- moffkalast 1y ago
  In poker?
deleted 1y ago
[deleted]
dsign 1y ago
I love the language of this article :-)... it may be florid, but that's quintessentially human. About the substance, I agree that there are fair grounds for concern, and it's not just about mathematics. The best case scenario is rejection and prohibition of uses of AI that fundamentally threaten human autonomy. It is theoretically possible to do so, but since capital and power are pro-AI[^1], getting there requires a social revolution that upends the current world order. Even if one were to happen, the results wouldn't last for too long. Unless said revolution were so utterly radical that would set us in a return trajectory to the middle ages (I have something of the sort published somewhere, check my profile!). I'm an optimist when it comes to the enabling power of AI for a select few. But I'm a pessimist otherwise: if the richest nation on Earth can't educate its citizens, what hope is there that humans will be able to supervise and control AI for long? Given our current trajectory, if nothing changes, we are set for civilization catastrophe. [^1]: Replacing expensive human labor is the most powerful modern economic incentive I know of. Money wants, money gets.
- awanderingmind 1y ago
  Thanks for the positive feedback on my writing style! Based on feedback in this thread it seems to be a divisive topic, haha.
  - npodbielski 1y ago
    I would say that I am envy that someone can write like that. I can't write in such manner in my native language, let alone in the second one: English. It is nice to read or hear someone speaking like that, considering we are surrounded by low quality, easy to consume content nowadays. And I am envy of such skill because I like to think about myself as not entirely being stupid, still I would never be able to write/speak this way because I just do not have an aptitude towards that.
    - deleted 1y ago
      [deleted]
    - awanderingmind 1y ago
lmm 1y ago
The camera didn't kill painting. Neither the bicycle nor the motor-car killed running. There are already subfields of mathematics where it's believed that all the interesting discoveries have been found and no-one is looking except for the occasional amateur - and other subfields where to even have a hope of doing cutting edge research you would need to both do multiple years of postgraduate study and then get accepted onto one of a small number of close-knit teams that are pushing that cutting edge on an industrial scale. So I don't see any reason to worry about the impact of AI. Unlike most fields with AI worries, mathematical research isn't even a significant employment area, and people with jobs doing it could almost certainly be doing something else for more money.
- jcelerier 1y ago
  > The camera didn't kill painting But it did. Painter used to be a trade where you could sell your painting skills as, well, a skill applicable for other than purely aesthetic reasons, simply because there were no other ways to document the world around you. It just isn't anymore because of cameras. Professional oil portrait painter isn't a career in 2025.
  - awanderingmind 1y ago
    Well, it is still a career, but it's very niche, and more attuned to 'art' than 'documenting the world'.
    - sgt101 1y ago
      and instead we have photographers who can document the world at a great volume. My Grandparents had no visual record of their wedding. My wife is a wedding photographer...
  - prennert 1y ago
    The Royal Society of Portrait Painters might disagree: https://therp.co.uk/artists/ https://therp.co.uk/artists/
gizajob 1y ago
[flagged]
skybrian 1y ago
I don’t share the author’s concern about a corporate takeover of mathematics. Most mathematics isn’t of commercial interest. Even when it is, it seems like there would often good reason to share it, like any other source code. Is Lean so different from other programming languages? Such libraries would need documentation, or nobody would know when to use them, and then sharing is pointless. If corporations build them, they would have to decide what to contribute to the commons and what to keep private. But that’s no different than any other language.
npodbielski 1y ago
I think people like author are positive about us, humanity, being able to build AI or something being very close to that. I am not. From the energy efficiency perspective human brain is very, very effective computational machine. Computers are not. Thinking about scale of infrastructure of network of computers being able to achieve similar capabilities and its energy consumption... it would be enormous. With big infrastructure comes high need of maintenance. This is costly and requires a lot of people just to prevent it from breaking down. With a lot of people being in one place, there socioeconomical cost, production, transportation needs to be build around such center. If you have centralized system, you are prone to attack from adversaries. In short I do not think we even close to what author is afraid of. We just closer to beginning to understand what is the need to actually start to think about building AI - if ever possible at all.
- Chris2048 1y ago
  > he energy efficiency perspective human brain is very, very effective computational machine Can you explain why you think that? Very often, mechanical efficiency outperforms biological. Humans have existed for thougsands of years, neurons even longer. Computers and AI and relatively recent, we haven't really begun to explore optimisation possibilities.
  - rcxdude 1y ago
    It may be possible to optimise silicon further, but the brain does all of its work with less than a hundred watts, while the silicon closest to its capabilities needs more like tens of kW.
    - deleted 1y ago
      [deleted]
    - Ukv 1y ago
      > while the silicon closest to its capabilities needs more like tens of kW. I think looking at power consumption for the very edge of what technology is just barely capble of may be misleading, since that's inherently at one extreme of the current cost-capability trade-off curve[0] and stands to drop the most drastically from efficiency improvements. You can now run models equivalent in capability to initial version of ChatGPT on sub-20w chips, for instance. Or, looking over a longer timeframe, we can now do far more on a 1-milliwatt chip[1] than on the 150kW ENIAC[2]. [0]: https://i.imgur.com/GydBGRG.png https://i.imgur.com/GydBGRG.png [1]: https://spectrum.ieee.org/syntiant-chip-plays-doom https://spectrum.ieee.org/syntiant-chip-plays-doom [2]: https://cse.engin.umich.edu/about/history/eniac-display/ https://cse.engin.umich.edu/about/history/eniac-display/
mathgradthrow 1y ago
The terrifying thing about lean and machine learning is not the idea that we will train computers on human written proof, but that we won't have to. With the rules of chess easily computed, a computer can use the bellman equations and self play to learn a policy that is vastly superior to human play, at least on the critical path. The state space of mathematics is pretty different from chess, but I think ultimately, mathematicians are just running something like A* on the space of propositions, with a custom heuristic that is learned by approximating the result of running A* with that heuristic. where your error is just the difference between the actual and predicted length of proof.
curtisszmania 1y ago
[dead]
credit_guy 1y ago
Test-driven development is not about tests. It's about writing code. The tests are there just in order to keep the bugs away. Mathematics is just proof-driven development. For an spectator it might look like mathematics is about writing proofs, but that's not different than seeing a software developer write a lot of tests. The proofs are the best tools against insidious logic bugs that the society of mathematics has come up with in the last few hundred years. Mathematicians would welcome automating all the proofs, just like software engineers are happy for code assistants to take over the task of writing tests.
acrophiliac 1y ago
"perhaps advanced ML research models will be more analogous to improvements in climbing gear, aiding the development of mountaineering as a sport, than an intrusion of corporate control into our minds". I would argue that GPS and Satellite-connected phones are already poisoning the wilderness experience.

We'll know that the time draws nearer when an AI confirms or refutes Mochizuki's proof of the abc conjecture. As of right now, I don't think they're capable of doing that. And, as they can't even check a very (very!) complex proof, they won't be able to conjure any inhumanly complex proofs de novo. Also: > To expand: what if the practice of mathematics becomes completely determined by the diktats of a vast capitalist machinery of proprietary machine learning models churning out proof after proof, and theory after theory, conjured from the aether of all possible true statements? I don't think that this is possible even in theory, as computational resources are limited and "the aether of all possible true statements" is incomprehensively vast. (There's a massive orders-of-magnitude difference in size between true-seeming-yet-false statements and the number of elementary particles in the visible universe. More statements than particles.) You can't brute force it.

bryanrasmussen 1y ago
also why would capitalists expand resources on churning out proof after proof when mathematical proofs are not patentable?
- auggierose 1y ago
  That will change quickly if capitalists see that as an obstacle. Right now, they don't really care about that, as for example software (much of which is just math) is already patentable in the US.
- awanderingmind 1y ago
  A reasonable question - another way of looking at it is that theorems are just a side effect of mathematical research. Much of the world economy depends on things like cryptography, which involves a bunch of theorems. The question is then 'what as yet undiscovered mathematical realms might models think up that could make people money'? It is hard to imagine what doesn't exist yet, but much harder to imagine that all potentially profitable mathematics has already been discovered. This could 'just' look like algorithmic improvements.
andyjohnson0 1y ago
> We'll know that the time draws nearer when an AI confirms or refutes Mochizuki's proof of the abc conjecture. As of right now, I don't think they're capable of doing that. And, as they can't even check a very (very!) complex proof, they won't be able to conjure any inhumanly complex proofs de novo. I agree, but... Spend time formalising a large part of existing mathematics and proofs, train a bunch of sufficiently powerful and generative models with that, and with cooperative problem solving and proof strategies, and give them access to proof assistants and adequate compute resources, and something interesting could happen. I suspect the barrier is finding a business model that would pay for this. Turning mathematics into an industrial, extruded-on-demand product might work, but I dont know who (except maybe the NSA) would stump-up the money.
n4r9 1y ago
Why would an AI confirmation or rejection be more convincing than the proof itself?
- esperent 1y ago
  Rejection: an incredibly complex proof can fall for (comparatively) simple reasons. If the AI scans the entire proof and says yep, there's the flaw, page 126 theorem X contradicts <well established known theorem> then a human can verify this without having to understand the whole proof. This could lead to the proof being rejected entirely, or fixed and strengthened. Confirmation: if the AI understands it well enough that we're even considering asking it to confirm the proof, then you can do all kinds of things. You can ask it to simplify the entire proof to make it easier for humans to verify. You can ask it questions about parts of the proof you don't understand. You can ask it if there's any interesting corollaries or applications in other fields. Maybe you can even ask it to rewrite the whole thing in LEAN (although, like the author, I know nothing about LEAN and have no idea if this would be useful).
- zarzavat 1y ago
  Presumably an AI would formalise the proof in a system such as Lean, then you only need to trust the kernel of that proof system. Rejecting a proof would be more complicated, because while for confirming a proof you only need to check that the main statement in the formalisation matches that of the conjecture, showing that a proof has been rejected requires knowledge of the proof itself (in general).
  - lblume 1y ago
    > requires knowledge of the proof itself (in general) Why? If a proof is wrong it has to be locally invalid, i.e. draw some inference which is invalid according to rules of logic. Of course the antecedent could have been defined pages earlier, but in and of itself the error must be local, right?
    - IsTom 1y ago
      Human-written proofs are not written in Lean to be checked easily and there'll be potentially many formalizations for written prose and only some of them will be what the author intended. You need to pick the right formalization before you can say that this proof has local errors.
awanderingmind 1y ago
I am not suggesting models will be capable of generating 'all' proofs - that is clearly impossible. Merely that they will get better at doing so, and there is no clear reason at the moment to believe they will never reach a human level of competence. If you have one model functioning at such a level, it is presumably trivial to have a million of them, none of which will need to be paid, housed, or sleep etc.

hliyan 1y ago

Considering that mathematics is, at its core, a language for defining relationships between quantities, and then relationships between those relationships, so on and so forth, I think it's fair to assume that the possible number of such relationships are infinite. Some of these relationships will obviously be useful in the real world, but they don't always have to be. I too, suspect that we can keep on building theorems on top of theorems with increasing complexity, until a point is reached that it becomes just too tedious (but not impossible) for a human being to work through the proof.

camjw 1y ago
> a language for defining relationships between quantities Could you expand on this? I don't see maths as a language for quantities specifically (i.e. what does symmetry have to do with quantities). > just too tedious (but not impossible) for a human being to work through the proof. Already happened with the four colour theorem arguably.
initramfs2 1y ago
just the zfc axioms alone are already infinite. It's an axiom schema ranging over an infinite number of actual statements. That's just statements, without even considering symbols as you're saying.
- bananaflag 1y ago
  Well you can just put the nbg instead, which is finitely axiomatizable
Someone 1y ago
> I think it's fair to assume that the possible number of such relationships are infinite That’s easily proven to be true. “Two plus two equals four” is a theorem, so is “three plus three equals six”, etc.
- im3w1l 1y ago
  Well I think the question should be how many interesting relationships there are.

N2yhWNXQN3k9 1y ago

This article is written in an unnecessarily extravagant style, IMO. Also, I appreciate anonymity, but, to my point > I live by myself in a remote mountain cave beyond the ken of civilised persons, and can only be contacted during a full moon, using certain arcane rites that are too horrible to speak of. Okay.

xdfgh1112 1y ago
Agreed if I had saw that first I wouldn't have clicked
BSDobelix 1y ago
>>I live by myself in a remote mountain cave = I live in California, and the nearest Starbucks is more than 20 miles away. >>can only be contacted during a full moon = As a night person, I am awake when the streetlight outside my house turns on. >>certain arcane rites that are too horrible to speak of = In order to contact me, you must install Microsoft Teams. Overall, it's not that bad, except for the MS team thing. ;)
- bubblyworld 1y ago
  The man is south african, we are geologically blessed and have a lot of pleasant remote mountain caves =)
  - BSDobelix 1y ago
    Okay, I will revert everything. The cave, the moon, and the rituals are all real. It's impressive how much reality is based on location :-)
    - bubblyworld 1y ago
      That's the spirit!
  - awanderingmind 1y ago
    True! I don't literally live in a cave, but fortunately not everyone is so allergic to whimsical language :D.

hackable_sand 1y ago

When does math become recreational for people?

coolcase 1y ago
At a young age?
srean 1y ago
When you do it with love
awanderingmind 1y ago
In my case, when you aren't paid to do it, and don't have (much) time to study it formally anymore.
plopilop 1y ago
How is that any different than people programming for fun?
moffkalast 1y ago
In poker?

deleted 1y ago

[deleted]

dsign 1y ago

I love the language of this article :-)... it may be florid, but that's quintessentially human. About the substance, I agree that there are fair grounds for concern, and it's not just about mathematics. The best case scenario is rejection and prohibition of uses of AI that fundamentally threaten human autonomy. It is theoretically possible to do so, but since capital and power are pro-AI[^1], getting there requires a social revolution that upends the current world order. Even if one were to happen, the results wouldn't last for too long. Unless said revolution were so utterly radical that would set us in a return trajectory to the middle ages (I have something of the sort published somewhere, check my profile!). I'm an optimist when it comes to the enabling power of AI for a select few. But I'm a pessimist otherwise: if the richest nation on Earth can't educate its citizens, what hope is there that humans will be able to supervise and control AI for long? Given our current trajectory, if nothing changes, we are set for civilization catastrophe. [^1]: Replacing expensive human labor is the most powerful modern economic incentive I know of. Money wants, money gets.

awanderingmind 1y ago
Thanks for the positive feedback on my writing style! Based on feedback in this thread it seems to be a divisive topic, haha.
- npodbielski 1y ago
  I would say that I am envy that someone can write like that. I can't write in such manner in my native language, let alone in the second one: English. It is nice to read or hear someone speaking like that, considering we are surrounded by low quality, easy to consume content nowadays. And I am envy of such skill because I like to think about myself as not entirely being stupid, still I would never be able to write/speak this way because I just do not have an aptitude towards that.
  - deleted 1y ago
    [deleted]
  - awanderingmind 1y ago

lmm 1y ago

The camera didn't kill painting. Neither the bicycle nor the motor-car killed running. There are already subfields of mathematics where it's believed that all the interesting discoveries have been found and no-one is looking except for the occasional amateur - and other subfields where to even have a hope of doing cutting edge research you would need to both do multiple years of postgraduate study and then get accepted onto one of a small number of close-knit teams that are pushing that cutting edge on an industrial scale. So I don't see any reason to worry about the impact of AI. Unlike most fields with AI worries, mathematical research isn't even a significant employment area, and people with jobs doing it could almost certainly be doing something else for more money.

jcelerier 1y ago
> The camera didn't kill painting But it did. Painter used to be a trade where you could sell your painting skills as, well, a skill applicable for other than purely aesthetic reasons, simply because there were no other ways to document the world around you. It just isn't anymore because of cameras. Professional oil portrait painter isn't a career in 2025.
- awanderingmind 1y ago
  Well, it is still a career, but it's very niche, and more attuned to 'art' than 'documenting the world'.
  - sgt101 1y ago
    and instead we have photographers who can document the world at a great volume. My Grandparents had no visual record of their wedding. My wife is a wedding photographer...
- prennert 1y ago
  The Royal Society of Portrait Painters might disagree: https://therp.co.uk/artists/ https://therp.co.uk/artists/

gizajob 1y ago

[flagged]

skybrian 1y ago

I don’t share the author’s concern about a corporate takeover of mathematics. Most mathematics isn’t of commercial interest. Even when it is, it seems like there would often good reason to share it, like any other source code. Is Lean so different from other programming languages? Such libraries would need documentation, or nobody would know when to use them, and then sharing is pointless. If corporations build them, they would have to decide what to contribute to the commons and what to keep private. But that’s no different than any other language.

npodbielski 1y ago

I think people like author are positive about us, humanity, being able to build AI or something being very close to that. I am not. From the energy efficiency perspective human brain is very, very effective computational machine. Computers are not. Thinking about scale of infrastructure of network of computers being able to achieve similar capabilities and its energy consumption... it would be enormous. With big infrastructure comes high need of maintenance. This is costly and requires a lot of people just to prevent it from breaking down. With a lot of people being in one place, there socioeconomical cost, production, transportation needs to be build around such center. If you have centralized system, you are prone to attack from adversaries. In short I do not think we even close to what author is afraid of. We just closer to beginning to understand what is the need to actually start to think about building AI - if ever possible at all.

Chris2048 1y ago
> he energy efficiency perspective human brain is very, very effective computational machine Can you explain why you think that? Very often, mechanical efficiency outperforms biological. Humans have existed for thougsands of years, neurons even longer. Computers and AI and relatively recent, we haven't really begun to explore optimisation possibilities.
- rcxdude 1y ago
  It may be possible to optimise silicon further, but the brain does all of its work with less than a hundred watts, while the silicon closest to its capabilities needs more like tens of kW.
  - deleted 1y ago
    [deleted]
  - Ukv 1y ago
    > while the silicon closest to its capabilities needs more like tens of kW. I think looking at power consumption for the very edge of what technology is just barely capble of may be misleading, since that's inherently at one extreme of the current cost-capability trade-off curve[0] and stands to drop the most drastically from efficiency improvements. You can now run models equivalent in capability to initial version of ChatGPT on sub-20w chips, for instance. Or, looking over a longer timeframe, we can now do far more on a 1-milliwatt chip[1] than on the 150kW ENIAC[2]. [0]: https://i.imgur.com/GydBGRG.png https://i.imgur.com/GydBGRG.png [1]: https://spectrum.ieee.org/syntiant-chip-plays-doom https://spectrum.ieee.org/syntiant-chip-plays-doom [2]: https://cse.engin.umich.edu/about/history/eniac-display/ https://cse.engin.umich.edu/about/history/eniac-display/

mathgradthrow 1y ago

The terrifying thing about lean and machine learning is not the idea that we will train computers on human written proof, but that we won't have to. With the rules of chess easily computed, a computer can use the bellman equations and self play to learn a policy that is vastly superior to human play, at least on the critical path. The state space of mathematics is pretty different from chess, but I think ultimately, mathematicians are just running something like A* on the space of propositions, with a custom heuristic that is learned by approximating the result of running A* with that heuristic. where your error is just the difference between the actual and predicted length of proof.

curtisszmania 1y ago

[dead]

credit_guy 1y ago

Test-driven development is not about tests. It's about writing code. The tests are there just in order to keep the bugs away. Mathematics is just proof-driven development. For an spectator it might look like mathematics is about writing proofs, but that's not different than seeing a software developer write a lot of tests. The proofs are the best tools against insidious logic bugs that the society of mathematics has come up with in the last few hundred years. Mathematicians would welcome automating all the proofs, just like software engineers are happy for code assistants to take over the task of writing tests.

acrophiliac 1y ago

"perhaps advanced ML research models will be more analogous to improvements in climbing gear, aiding the development of mountaineering as a sport, than an intrusion of corporate control into our minds". I would argue that GPS and Satellite-connected phones are already poisoning the wilderness experience.