AI is discovering patterns in pure mathematics that have never been seen before
sciencealert.com
sciencealert.com
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...
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.
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)
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!
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)
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.∎
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.
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.
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.
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]
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.
This is not true. Doron Zeilberger has long used Shalosh Ekhad to formulate conjectures: https://www.wired.com/2013/03/computers-and-math .
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! :)
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.
Edit: Look, sniper: unfounded statements are cheap. Anyone can state 'A is B': as a form, it is largely worthless.
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
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.
But you could still say: A mathematical structure is analysing mathematics.
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.
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?