AI is discovering patterns in pure mathematics that have never been seen before(sciencealert.com)
sciencealert.com
AI is discovering patterns in pure mathematics that have never been seen before
https://www.sciencealert.com/ai-is-discovering-patterns-in-pure-mathematics-that-have-never-been-seen-before
42 comments
[deleted]
Just to add some more detail to this. The first link [0] you referenced is one I submitted a while ago. It did not gain much attention and I was not really surprised since the same underlying research was being reported by different sources in variously vague ways.
Anyway, I received an email from HN yesterday saying they wanted to put it on the “second-chance pool” and I could do so by clicking a link to repost it. I never received an email from HN before and I was curious what would happen, so I clicked to repost, and of course it then shot to the top of the front page.
0: https://news.ycombinator.com/item?id=29514642
Anyway, I received an email from HN yesterday saying they wanted to put it on the “second-chance pool” and I could do so by clicking a link to repost it. I never received an email from HN before and I was curious what would happen, so I clicked to repost, and of course it then shot to the top of the front page.
0: https://news.ycombinator.com/item?id=29514642
Not only has it been on the front page a bunch; each time it’s posted, it’s further and further through the game of telephone from science to pop journalism, and less and less accurate.
It might be interesting to map the quality of the hn conversations to the distance from the source in either time or internet distance.
Thanks! Macroexpanded:
DeepMind’s AI helps untangle the mathematics of knots - https://news.ycombinator.com/item?id=29514642 - Dec 2021 (61 comments)
DeepMind cracks 'knot' conjecture that bedeviled mathematicians for decades - https://news.ycombinator.com/item?id=29466753 - Dec 2021 (3 comments)
Can deep learning help mathematicians build intuition? - https://news.ycombinator.com/item?id=29424749 - Dec 2021 (28 comments)
Exploring the beauty of pure mathematics in novel ways - https://news.ycombinator.com/item?id=29405380 - Dec 2021 (4 comments)
Mathematicians Find Structure in Biased Polynomials - https://news.ycombinator.com/item?id=29208141 - Nov 2021 (8 comments)
DeepMind’s AI helps untangle the mathematics of knots - https://news.ycombinator.com/item?id=29514642 - Dec 2021 (61 comments)
DeepMind cracks 'knot' conjecture that bedeviled mathematicians for decades - https://news.ycombinator.com/item?id=29466753 - Dec 2021 (3 comments)
Can deep learning help mathematicians build intuition? - https://news.ycombinator.com/item?id=29424749 - Dec 2021 (28 comments)
Exploring the beauty of pure mathematics in novel ways - https://news.ycombinator.com/item?id=29405380 - Dec 2021 (4 comments)
Mathematicians Find Structure in Biased Polynomials - https://news.ycombinator.com/item?id=29208141 - Nov 2021 (8 comments)
I haven’t seen it yet so it’s alright for me.
This is the dirty secret of reposts. It is only people who spend their lives on HN and see (and somehow remember) every single previous post that care about reposts.
The review paper is really interesting: "Machine-Learning Mathematical Structures"
Thanks for this interesting and readable paper!
[deleted]
That’s actually pretty cool (and not the hyperbole that articles about use of AI in science usually are.)
Current-gen Deep Leaning systems are really good at “riffing on” text inputs. So feed them a bunch of known math conjectures, and new conjectures should fall out.
Not that this is a new thing — mathematicians have been using various procedural generation methods to formulate conjectures since Prolog was invented. But the Deep Learning text AIs make this much easier — you don’t need to model the domain, the syntax of a mathematical conjecture; these AIs discover that much for you. So you can more quickly and cheaply apply these modern methods to exploring conjecture-space in new subdisciplines.
And of course, this still has nothing to do with what futurists were expecting ML to eventually do for math (generating proofs, putting mathematicians out of a job); instead, something a lot less obvious as “useful work”, but useful nevertheless!
Current-gen Deep Leaning systems are really good at “riffing on” text inputs. So feed them a bunch of known math conjectures, and new conjectures should fall out.
Not that this is a new thing — mathematicians have been using various procedural generation methods to formulate conjectures since Prolog was invented. But the Deep Learning text AIs make this much easier — you don’t need to model the domain, the syntax of a mathematical conjecture; these AIs discover that much for you. So you can more quickly and cheaply apply these modern methods to exploring conjecture-space in new subdisciplines.
And of course, this still has nothing to do with what futurists were expecting ML to eventually do for math (generating proofs, putting mathematicians out of a job); instead, something a lot less obvious as “useful work”, but useful nevertheless!
I think the challenge is to only/mostly generate interesting conjectures. For example “All natural numbers are larger than minus ten” or “no prime is divisible by 10,000” are valid theorems, but not interesting, and could have zillions of equally uninteresting variations.
There often are zillions of ways to phrase a theorem that aren’t too obvious, initially. For example, https://en.wikipedia.org/wiki/Tic-tac-toe#Variations gives a few games that are isomorphic to tic-tac-toe.
I fear a theorem generator would come up with lots of such theorem variants, with most of them being uninteresting to mathematicians (such isomorphies typically are considered interesting if they join two fields hitherto considered disjunct or if it takes mathematicians long to figure out that they are essentially, synonymous)
There often are zillions of ways to phrase a theorem that aren’t too obvious, initially. For example, https://en.wikipedia.org/wiki/Tic-tac-toe#Variations gives a few games that are isomorphic to tic-tac-toe.
I fear a theorem generator would come up with lots of such theorem variants, with most of them being uninteresting to mathematicians (such isomorphies typically are considered interesting if they join two fields hitherto considered disjunct or if it takes mathematicians long to figure out that they are essentially, synonymous)
I suspect if you created some kind of a graph between related theorems, you could identify the interesting ones by how many edges a particular node has, or by whether or not it is a part of a previously unknown shortcut between such nodes. I also suspect some form of this has already been done. I know this problem has been identified and there are all sorts of ideas to try to come up with a criteria for “interesting”. Don’t know what you call that area of research or what the latest is/am not a professional mathematician.
But yeah, a world in which everyone becomes dependent on computer generated maps to parse through seas of computer generated jargon seems less like a world where people do math and more like a world where people do mathematically informed seances.
Finding isomorphisms might also be misleading. Formalizing some set of assumptions for a theorem might identify non existent similarities that have more to do with using the same meta language to formalize things rather than the intended meaning of some of the theorems.
Again, pretty sure these issues are well understood, and people smarter than me are doing things to mitigate them, but I think there’s a real big problem here related to translating machine created discoveries into a meta language a computer can make sense of and then back into a language humans can understand better and verify without relying on the machine.
But yeah, a world in which everyone becomes dependent on computer generated maps to parse through seas of computer generated jargon seems less like a world where people do math and more like a world where people do mathematically informed seances.
Finding isomorphisms might also be misleading. Formalizing some set of assumptions for a theorem might identify non existent similarities that have more to do with using the same meta language to formalize things rather than the intended meaning of some of the theorems.
Again, pretty sure these issues are well understood, and people smarter than me are doing things to mitigate them, but I think there’s a real big problem here related to translating machine created discoveries into a meta language a computer can make sense of and then back into a language humans can understand better and verify without relying on the machine.
> ... and could have zillions of equally uninteresting variations.
Which themselves could generate uninteresting theorems:
Theorem: The set of such uninteresting variations of "All natural numbers are larger than minus ten" is countably infinite.
Proof: Let the uninteresting variations of "All natural numbers are larger than minus ten" be represented as "All natural numbers are larger than minus n" where n is a natural number. Since there exists a one-to-one correspondence between the natural numbers and the natural numbers, the set of uninteresting variations of "All natural numbers are larger than minus ten" is countably infinite.∎
Which themselves could generate uninteresting theorems:
Theorem: The set of such uninteresting variations of "All natural numbers are larger than minus ten" is countably infinite.
Proof: Let the uninteresting variations of "All natural numbers are larger than minus ten" be represented as "All natural numbers are larger than minus n" where n is a natural number. Since there exists a one-to-one correspondence between the natural numbers and the natural numbers, the set of uninteresting variations of "All natural numbers are larger than minus ten" is countably infinite.∎
The set of all theorems, or even all statements, is countably infinite. The symbolic representation of a statement is only a string of characters and can be converted to a very large integer.
Even our notion of uncountable sets is itself countable, in that we use language to reason about them. It actually pretty sad - we’re are two-dimensional creatures in the three-dimensional world.
Even our notion of uncountable sets is itself countable, in that we use language to reason about them. It actually pretty sad - we’re are two-dimensional creatures in the three-dimensional world.
I thought this critical paper about the original paper (and maybe rather the news or marketing about the original paper) was fair and helps put things into perspective:
https://arxiv.org/abs/2112.04324
So a relatively simple neural net finds statistical regularity. Personally I agree that it probably could have been done with ordinary statistics. I'm surprised at how viral this story has become.
So a relatively simple neural net finds statistical regularity. Personally I agree that it probably could have been done with ordinary statistics. I'm surprised at how viral this story has become.
Of course we all remember that discovering new theorems in mathematics and new _proofs_ of theorems in mathematics has been done to death since the beginnings of AI.
For example, see the wikipedia page on the Automated Mathematician (1977):
https://en.wikipedia.org/wiki/Automated_Mathematician
And follow the links from that article to (stub) articles on HR (2016):
https://en.wikipedia.org/wiki/HR_(software)
And Graffiti (1989):
https://en.wikipedia.org/wiki/Graffiti_(program)
And then jump over to the Automated Theorem Proving article:
https://en.wikipedia.org/wiki/Automated_theorem_proving
And from there to the article on the Logic Theorist (1956):
https://en.wikipedia.org/wiki/Logic_Theorist
Which, I quote from the wikipedia article:
Logic Theorist is a computer program written in 1956 by Allen Newell, Herbert A. Simon and Cliff Shaw.[1] It was the first program deliberately engineered to perform automated reasoning and is called "the first artificial intelligence program".[a] It would eventually prove 38 of the first 52 theorems in Whitehead and Russell's Principia Mathematica, and find new and more elegant proofs for some.[3]
For example, see the wikipedia page on the Automated Mathematician (1977):
https://en.wikipedia.org/wiki/Automated_Mathematician
And follow the links from that article to (stub) articles on HR (2016):
https://en.wikipedia.org/wiki/HR_(software)
And Graffiti (1989):
https://en.wikipedia.org/wiki/Graffiti_(program)
And then jump over to the Automated Theorem Proving article:
https://en.wikipedia.org/wiki/Automated_theorem_proving
And from there to the article on the Logic Theorist (1956):
https://en.wikipedia.org/wiki/Logic_Theorist
Which, I quote from the wikipedia article:
Logic Theorist is a computer program written in 1956 by Allen Newell, Herbert A. Simon and Cliff Shaw.[1] It was the first program deliberately engineered to perform automated reasoning and is called "the first artificial intelligence program".[a] It would eventually prove 38 of the first 52 theorems in Whitehead and Russell's Principia Mathematica, and find new and more elegant proofs for some.[3]
it may be done to death but it certainly doesn't seem like a solved problem?
I'm a fan of deepmind and all, but this story has been way overblown based on what I saw in the actual code. There's nothing particularly new about mathematicians using computers to investigate and make conjectures, even if you add ML into it.
> but this story has been way overblown based on what I saw in the actual code.
Could you expand on this? What code did you see, where, and doing what? Were you part of this team?
> There's nothing particularly new about mathematicians using computers to investigate and make conjectures, even if you add ML into it.
I think you're being needlessly reductive here. The article itself explicitly states that "using computers" is not what's new.
Could you expand on this? What code did you see, where, and doing what? Were you part of this team?
> There's nothing particularly new about mathematicians using computers to investigate and make conjectures, even if you add ML into it.
I think you're being needlessly reductive here. The article itself explicitly states that "using computers" is not what's new.
As is typical in most AI coverage. The amount of white lies and fake news in scientific journalism is insane
> "While mathematicians have used machine learning to assist in the analysis of complex data sets, this is the first time we have used computers to help us formulate conjectures or suggest possible lines of attack for unproven ideas in mathematics."
This is not true. Doron Zeilberger has long used Shalosh Ekhad to formulate conjectures: https://www.wired.com/2013/03/computers-and-math .
This is not true. Doron Zeilberger has long used Shalosh Ekhad to formulate conjectures: https://www.wired.com/2013/03/computers-and-math .
Pedantic note: Shalosh B. Ekhad. The middle initial is important, because the name derives from the fact that the original Shalosh B. Ekhad was an AT&T 3B1 computer. ("Shalosh" is the HEbrew name for the number 3, and "ekhad" is the Hebrew name for the number 1.)
Thank you! I did not realise that.
I find that an often under-appreciated perspective around big networks is the information-theoretical one, or at the risk of oversimplifying: the compression one. (The deep relationships between learning theory and information theory are of course well-known to researchers and sophisticated practitioners, but IMHO don’t get enough airtime).
When you think about training a (not terribly overfit) model as a crop in the Fourier domain, a lot of these results are fairly natural to intuit about, which of course takes nothing away from how cool they are! :)
When you think about training a (not terribly overfit) model as a crop in the Fourier domain, a lot of these results are fairly natural to intuit about, which of course takes nothing away from how cool they are! :)
Consider Greg Egan : Diaspora. It's a sci fi novel
In it there's something called "The Science Mines".
In the Science Mines a researcher (An AI person) explores paths of logic and conjecture, tunneling into the raw earth of "all possibilities". Discovering patterns, theorems.
We have invented The Science Mines.
In it there's something called "The Science Mines".
In the Science Mines a researcher (An AI person) explores paths of logic and conjecture, tunneling into the raw earth of "all possibilities". Discovering patterns, theorems.
We have invented The Science Mines.
http://fenn.freeshell.org/Science.pdf - paper doing something similar but using evolutionary techniques like symbolic regression to find physical laws from real world data
[deleted]
Sounds like Max Cohen at work, doesn't it?
Alternate title: AI (a man-made concept) is discovering patterns in another man-made concept.
I would disagree with the idea that maths is man-made. It is discovered. If it were man made, then we should have power to change it as we wish.
But you could still say: A mathematical structure is analysing mathematics.
But you could still say: A mathematical structure is analysing mathematics.
I would disagree there are quick and easy answers to the question of whether math is man-made or discovered. What is the qualitative difference between discovery and invention?
Consider the product of no factors being equal to the multiplicative identity. Is that a discovery or a choice made because it is more useful? Is it a discovery because we 'discovered' it was more useful?
Consider the product of no factors being equal to the multiplicative identity. Is that a discovery or a choice made because it is more useful? Is it a discovery because we 'discovered' it was more useful?
One way I’ve seen it put, that resonates with me, is that axioms are invented but theorems are discovered. That is nicely self-evident. The idea that axioms are also discovered is … iffy, but it happens in some cases. E.g., discovering that your theory is unsound and the only way to fix it is by adding the obvious axiom.
You mean physical structures. Math is just glyphs we use to cart around awareness of the motions of this reality.
I know it’s romantic to escape into the neverending-ness of reality, but we exist in a pretty well established perimeter of physical constraints, and we have yet to find even a theory that would let us break them.
A few academic tricks here and there is hardly concrete proof we can.
I think we’re looking the wrong way. What if we’re each a metaverse forced to live literally?
Give me designer drugs that bootstrap such a detailed hallucination, I think it happened. Way less wasteful than these toys like VR we just throwaway.
Don’t make the math literal, make the cognitive simulation so detailed it feels like it’s literal.
Maybe aliens didn’t die off. They just took resource consumption seriously.
I know it’s romantic to escape into the neverending-ness of reality, but we exist in a pretty well established perimeter of physical constraints, and we have yet to find even a theory that would let us break them.
A few academic tricks here and there is hardly concrete proof we can.
I think we’re looking the wrong way. What if we’re each a metaverse forced to live literally?
Give me designer drugs that bootstrap such a detailed hallucination, I think it happened. Way less wasteful than these toys like VR we just throwaway.
Don’t make the math literal, make the cognitive simulation so detailed it feels like it’s literal.
Maybe aliens didn’t die off. They just took resource consumption seriously.
What do you imply.
That math is invented not discovered
Mathematical notation is invented but what about the patterns it describes? Did someone invent the notion of exponential growth or decay? Or did we discover this mathematical pattern in many different areas of study?
Also, from Wikipedia: "Most of mathematical activity consists of discovering and proving (by pure reasoning) properties of abstract objects. These objects are either abstractions from nature (such as natural numbers or "a line"), or (in modern mathematics) abstract entities that are defined by their basic properties, called axioms." - https://en.wikipedia.org/wiki/Mathematics
Also, from Wikipedia: "Most of mathematical activity consists of discovering and proving (by pure reasoning) properties of abstract objects. These objects are either abstractions from nature (such as natural numbers or "a line"), or (in modern mathematics) abstract entities that are defined by their basic properties, called axioms." - https://en.wikipedia.org/wiki/Mathematics
I agree that some mathematical concepts, such as exponential growth, are expressed in nature. But does the fact that a thing is expressed in nature imply that it cannot be invented? And what of mathematical concepts not expressed in nature?
On a different point, I'd argue that all conceptual inventions are discoveries. So, showing that a mathematical concept was discovered would not be enough to prove it was not invented.
On a different point, I'd argue that all conceptual inventions are discoveries. So, showing that a mathematical concept was discovered would not be enough to prove it was not invented.
That's oracular...
Edit: Look, sniper: unfounded statements are cheap. Anyone can state 'A is B': as a form, it is largely worthless.
Edit: Look, sniper: unfounded statements are cheap. Anyone can state 'A is B': as a form, it is largely worthless.
https://news.ycombinator.com/item?id=29514642
https://news.ycombinator.com/item?id=29424749
https://news.ycombinator.com/item?id=29405380
https://news.ycombinator.com/item?id=29208141
Finding mathematical patterns and relations by fitting expressive functions has actually been a common technique in experimental mathematics (https://en.wikipedia.org/wiki/Experimental_mathematics) for a while.
In the last few years, neural networks in particular have been used a lot in areas of math related to string theory, where one tries to find structures on certain topological spaces that preserve or generate symmetries of the resulting physics. Here's a review that might be interesting:
https://arxiv.org/abs/2101.06317
Unfortunately, none of these mathematicians have the marketing prowess of a multi-billion dollar company...