31–40 of 43 posts
I don't normally complain about this, but that result has been at least four times on the front page in the last two weeks: 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…
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…
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#Var…
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.∎
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…
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]
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…
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#Var…
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.
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.
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.
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?
I don't normally complain about this, but that result has been at least four times on the front page in the last two weeks: 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…
I don't normally complain about this, but that result has been at least four times on the front page in the last two weeks: 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…
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)
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 Graff…