8 ms·

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 “

by derefr 5y ago

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!

Someone 5y ago
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 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)
- cgriswald 5y ago
  > ... 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.∎
  - DenisM 5y ago
    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.
- didericis 5y ago
  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.
fault1 5y ago
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 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.

by derefr 5y ago

Someone 5y ago

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 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)

cgriswald 5y ago
> ... 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.∎
- DenisM 5y ago
  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.
didericis 5y ago
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.

fault1 5y ago

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 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.