The mathematics are above my intellectual capacities, but I still find the man and his lifestyle fascinating. Though I admit his heart attack probably wasn't a coincidence, sadly.
I wonder if national, institutional, or otherwise "eccentric" sponsorships (encouraging a similar migrant-madman approach to academic cultivation) of some of the folks on HN wouldn't lead to meaningful discoveries in CS.
I often see comments that some of the users here long to "make a computer do neat tricks all day", and I can't help but think meager sponsorship could go a long way in this area. Existing grant structures, being much more traditional, are constrained by their cost.
When OpenAI posted about their 10 breakthroughs, I saw lots of career research mathematicians say things mostly along the lines of “I don’t understand any of this it’s way over my head”.
Are we missing the forest for the trees here? If a math problem falls in the forest but nobody is around to understand it does it make a sound?
How can we possibly make use of these breakthroughs if we don’t understand them? How could we ever make anything useful with them?
Are we ready to just let go of our intellectual faculties and give them to a giant supercomputer nobody understands? How do we tell truth from fiction?
> How can we possibly make use of these breakthroughs if we don’t understand them? How could we ever make anything useful with them?
Theoretical science isn't about usefulness per se, but knowledge and understanding for its own sake, so a better way to say this is to point out that you only benefit in such cases if you understand things yourself. If understanding is the goal - which it is in the case of true theory - then the only way to attain that goal is to actually attain understanding. What good is it if an LLM produces a valid proof, but no one grasps it? This isn't like digging a ditch where it doesn't matter who does it or how he does it as long as you have a ditch. Here, the ditch is knowledge, as it were.
It's more like FOSS project using and you ask a developer who works at a different company how to build this project and he says "I don't know automake, perl and there are lots of macros"
What are the odds that this random FOSS project has solved the problem of building software and nobody noticed. Close to 0. Don't confuse accidental complexity for transcendental depth.
something i've just realized : today long-standing maths problems are falling. It's great intellectually but won't probably have an immediate impact on our lives.
Now, what will happen once long-standing physics ( and chemistry and biology) problems will start to fall and at the same rate ?
Then we're going to enter a totally different world.
For example, protein folding has been figured out by AI. This was a very big moment for science and yielded a nobel prize. Alphafold 1 happened 4 years before the first version of ChatGPT and the LLM craze we see today.
But yeah, most problems in physics, chemistry or biology require labs on top of actual hard thinking. You need to be able to design experiments in a certain way. Once you have the funding, the right tools, the right people to use those tools, then you can use LLMs to increase the speed of the calculations and so on.
The AIs seem to have some combination of very broad familiarity with math (enabling relevant things from other subfields to be brought in to the proof) as well as patience and "sitzfleisch" (stamina in working through details even if they aren't immediately obviously promising.)
An obvious area for improvement would be automated generation of new conjectures and attempts to prove (or disprove) them, with the discovered arguments then being used as training for refined models. This will require autoformalization to check the results as there will be too many for manual verification.
Disappointing lack of "Why" in an article that starts with it.
Are they actually doing something new and novel, or are they just absorbing that "a=b as was proven in transcendental hyper-circular group theory; and b=c was proven in universal quantum superposition"; and they're the first to find the connection that a=c? And several of the problems are counterexamples, not novel proofs of correctness?
Its fascinating either way, but it'd be nice to actually understand more of what is happening.
It seems that AIs are really good at finding counterexamples now.
Even if progress by AIs in proving conjectures lags, it seems likely that AIs collectively will, in the next few years, find counterexamples to nearly all the Erdős (and other) conjectures that are actually false and also provably false.
That means we will able to assume that nearly all the remaining conjectures are either true or undecidable.
Surely, that's good for folks who just want to know where the truth boundaries in mathematics lie.
It's obviously causing a lot of soul-searching amongst professional mathematicians.
Arguably, they should have given less weight for the last 100 years to Hardy's view in 'A Mathematician's Apology' [0]:
> It is a melancholy experience for a professional mathematician to find himself writing about mathematics. The function of a mathematician is to do something, to prove new theorems, to add to mathematics, and not to talk about what he or other mathematicians have done.
Rota takes a much more balanced view in 'Indiscrete Thoughts' [1].
"Problem Solvers" take Hardy's view:
> ... The mathematical concepts required to state mathematical problems are tacitly assumed to be eternal and immutable. Mathematical exposition is regarded as an inferior undertaking. ...
While for "theorizers":
> Mathematical exposition is considered a more difficult undertaking than mathematical research.
If professional mathematicians can reinvent themselves, there will be plenty of work left to do to explain the results of AIs to other humans.
There probably needs to be a new career path into professional pure mathematics other than doing novel research in a PhD.
> That means we will able to assume that nearly all the remaining conjectures are either true or undecidable
I mean, we could. But it doesn't really make sense to think that AIs are perfect at finding counterexamples, just because they are good (or even better than us). My general opinion is that they are orthagonally intelligent, that is, they are intelligent in an entirely different way to the way that people are. They are undoubtably clever, but the distance between when they are better than us at their best skill (or even most skills) and when they are better than us in all aspects is going to be MASSIVE.
Counterexamples can be decidable and arbitrarily ugly or difficult to find. If you know anything about mathematics it's trivially simple things can yield extremely complex structures. And that can absolutely include terse conjectures whose solutions are in fact decidable but only with proofs that would consume more than a bit of memory for every particle in the universe. Not logically undecidable, but physically impossible to prove in our physical universe.
Further down the scale are ones that are decidable only by machines that we would never have the wherewithal to construct, even though they could physically be constructed with the material we have to work with.
> “A big problem is AI is being used a lot by people who aren’t mathematicians, who don’t have a huge mathematical background and are not capable of verifying the output,” Bloom said. “They like to move fast, ask their AI to check it, it grows and grows. We’re seeing a lot more of these 100- to 200-page papers that people are posting. ‘I solved this theorem; I got AI to generate the proof and check the proof and write the paper.’ But no human has read it, and no human is going to read it. It’s a huge challenge now.”
Mathematics has the same problem as open source projects that are overwhelmed with AI slop!
19 comments
[ 0.21 ms ] story [ 10.8 ms ] threadI wonder if national, institutional, or otherwise "eccentric" sponsorships (encouraging a similar migrant-madman approach to academic cultivation) of some of the folks on HN wouldn't lead to meaningful discoveries in CS.
I often see comments that some of the users here long to "make a computer do neat tricks all day", and I can't help but think meager sponsorship could go a long way in this area. Existing grant structures, being much more traditional, are constrained by their cost.
The whole article is an ad that covertly or overtly inserts how websites are built with ChatGPT, how humans say that AI is better than them etc.
This is incidentally the future of chatbots. I could not have written this comment without Illy Espresso. Would you like to find a cafe near you?
Are we missing the forest for the trees here? If a math problem falls in the forest but nobody is around to understand it does it make a sound?
How can we possibly make use of these breakthroughs if we don’t understand them? How could we ever make anything useful with them?
Are we ready to just let go of our intellectual faculties and give them to a giant supercomputer nobody understands? How do we tell truth from fiction?
Theoretical science isn't about usefulness per se, but knowledge and understanding for its own sake, so a better way to say this is to point out that you only benefit in such cases if you understand things yourself. If understanding is the goal - which it is in the case of true theory - then the only way to attain that goal is to actually attain understanding. What good is it if an LLM produces a valid proof, but no one grasps it? This isn't like digging a ditch where it doesn't matter who does it or how he does it as long as you have a ditch. Here, the ditch is knowledge, as it were.
What are the odds that this random FOSS project has solved the problem of building software and nobody noticed. Close to 0. Don't confuse accidental complexity for transcendental depth.
Isn't that what people from more practical sciences said about math anyways?
All math is eventually applied math.
Now, what will happen once long-standing physics ( and chemistry and biology) problems will start to fall and at the same rate ?
Then we're going to enter a totally different world.
But yeah, most problems in physics, chemistry or biology require labs on top of actual hard thinking. You need to be able to design experiments in a certain way. Once you have the funding, the right tools, the right people to use those tools, then you can use LLMs to increase the speed of the calculations and so on.
There have been other discoveries though by deepmind: https://deepmind.google/blog/millions-of-new-materials-disco...
The AIs seem to have some combination of very broad familiarity with math (enabling relevant things from other subfields to be brought in to the proof) as well as patience and "sitzfleisch" (stamina in working through details even if they aren't immediately obviously promising.)
An obvious area for improvement would be automated generation of new conjectures and attempts to prove (or disprove) them, with the discovered arguments then being used as training for refined models. This will require autoformalization to check the results as there will be too many for manual verification.
Are they actually doing something new and novel, or are they just absorbing that "a=b as was proven in transcendental hyper-circular group theory; and b=c was proven in universal quantum superposition"; and they're the first to find the connection that a=c? And several of the problems are counterexamples, not novel proofs of correctness?
Its fascinating either way, but it'd be nice to actually understand more of what is happening.
Even if progress by AIs in proving conjectures lags, it seems likely that AIs collectively will, in the next few years, find counterexamples to nearly all the Erdős (and other) conjectures that are actually false and also provably false.
That means we will able to assume that nearly all the remaining conjectures are either true or undecidable.
Surely, that's good for folks who just want to know where the truth boundaries in mathematics lie.
It's obviously causing a lot of soul-searching amongst professional mathematicians.
Arguably, they should have given less weight for the last 100 years to Hardy's view in 'A Mathematician's Apology' [0]:
> It is a melancholy experience for a professional mathematician to find himself writing about mathematics. The function of a mathematician is to do something, to prove new theorems, to add to mathematics, and not to talk about what he or other mathematicians have done.
Rota takes a much more balanced view in 'Indiscrete Thoughts' [1].
"Problem Solvers" take Hardy's view:
> ... The mathematical concepts required to state mathematical problems are tacitly assumed to be eternal and immutable. Mathematical exposition is regarded as an inferior undertaking. ...
While for "theorizers":
> Mathematical exposition is considered a more difficult undertaking than mathematical research.
If professional mathematicians can reinvent themselves, there will be plenty of work left to do to explain the results of AIs to other humans.
There probably needs to be a new career path into professional pure mathematics other than doing novel research in a PhD.
[0] https://en.wikipedia.org/wiki/A_Mathematician%27s_Apology
[1] https://ncatlab.org/nlab/show/Gian-Carlo+Rota
https://ncatlab.org/nlab/show/Gian-Carlo+Rota
I mean, we could. But it doesn't really make sense to think that AIs are perfect at finding counterexamples, just because they are good (or even better than us). My general opinion is that they are orthagonally intelligent, that is, they are intelligent in an entirely different way to the way that people are. They are undoubtably clever, but the distance between when they are better than us at their best skill (or even most skills) and when they are better than us in all aspects is going to be MASSIVE.
Further down the scale are ones that are decidable only by machines that we would never have the wherewithal to construct, even though they could physically be constructed with the material we have to work with.
Mathematics has the same problem as open source projects that are overwhelmed with AI slop!