11 ms·

How close are computers to automating mathematical reasoning?

100 points by auggierose 6y ago

Kednicma 6y ago
It's irresponsible to not mention that a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible, in the sense that we cannot just ask a computer to find a proof or refutation of Goldbach's Conjecture or other "Goldbach-type" statement and have it do any better than a person. In that sense, no, computers will never fully automate mathematical reasoning, because mathematical reasoning cannot be fully automated. What we can automate, and have successfully automated many times over, is proof checking. In that sense, yes, computers have already fully automated mathematical reasoning, because checking proofs is fully formalized and mechanized. I think that what people really ought to be asking for is the ease with which we find new results and communicate them to others. In that sense, computer-aided proofs can be hard to read and so there is much work to be done in making them easier to communicate to humans. Similarly, there is interesting work being done on how to make computer-generated proofs which use extremely-high-level axiom schemata to generate human-like handwaving abstractions. I'm still not sure how I feel about the ATP/ITP terminology used here. ATPs are either of the weak sort that crunch through SAT, graphs, and other complete-but-hard problems, or the strong sort which are impossible. Meanwhile, folks have drifted from "interactive" to "assistant", and talk of "proof assistants" as tools which, like a human, can write down and look at sections of a proof in isolation, but cannot summon complete arbitrary proofs from its own mind. Edit: One edit will be quicker than two replies and I tend to be "posting too fast". The main point is captured well by [0], but they immediately link to [1], the central result, which links to [2], an important corollary. At this point, I'm just going to quote WP: > The first [Gödel] incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. > The second [Gödel] incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency. > Informally, [Tarski's Undefinability] theorem states that arithmetical truth cannot be defined in arithmetic. I recognize that these statements may seem surprising, but they are provable and you should convince yourself of them. I recently reviewed [3] and found it to be a very precise and complete introduction to all of the relevant ideas; there's also GEB if you want something more fun. [0] https://en.wikipedia.org/wiki/Automated_theorem_proving#Decidability_of_the_problem https://en.wikipedia.org/wiki/Automated_theorem_proving#Deci... [1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [2] https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo... [3] https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf https://www.logicmatters.net/resources/pdfs/godelbook/GodelB...
- lordnacho 6y ago
  > a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible Have you got some links? Sounds very interesting.
  - a_humean 6y ago
    He is refering to the late 19th and early 20th century work on the foundations of mathematics amoung mathematicans and philosophers. They attempted to fully formalise mathematics. Serveral approaches and schools in mathematics all hit various paradoxes, often of the same kind, and this ultimately culminated in Godel's incompleteness theorems: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... https://plato.stanford.edu/entries/goedel-incompleteness https://plato.stanford.edu/entries/goedel-incompleteness
  - umvi 6y ago
    There's also a thing called "the halting problem" which is related to this. Because without the halting problem you could solve any mathematical proof by simply turning it into a computer program that brute forces the problem domain and calculating whether the the program will terminate or not. Of course, this is impossible.
    - sukilot 6y ago
      That's a bit backwards. The halting problem is a computer-flavored variant of Gödel's work. A very simple part -- it's essentially a computer program that says "The program that produced this string is lying".
- bigyikes 6y ago
  As someone unfamiliar with the results you describe, why can’t a machine do better than a human? A smart human is better at writing proofs than a dumb one. If we had a highly advanced general artificial intelligence, why couldn’t it generate better results than the smart humans?
ogogmad 6y ago
People bringing up GIT (Goedel's Incompleteness Theorem) don't understand that GIT is a limitation of formal logic which affects human mathematicians as much as computer-based mathematicians. Both humans and computers are forced to work with a recursively enumerable set of axioms when constructing mathematical proofs, and so therefore are bound by the same limitations. Also, if you can check a proof, then you can certainly automatically construct a proof, merely by dove-tailing over all possible proofs and checking whether they're correct and imply the desired conjecture. In other words, using GIT when discussing proof automation is irrelevant.
- __MatrixMan__ 6y ago
  I agree that GIT limits human provers as much as it limits automated ones, but I don't agree that it's irrelevant to the issue. A human mathematician can lean on intuition in ways that a computer can't. Given a theorem that resists proof, a human might develop a feel for whether it's worth continuing to prove via conventional means or whether the troublesome territory is better approached from a different axiom set. That intuition may be driven by the problematic theorem being one of the true-but-unprovable ones that Godel assures us exists without that cause being apparent to the mathematician. The automated prover, on the other hand, faces a halting problem here. Unless it is given some explicit reason to expect that the target is not attainable, it might try forever. So such a prover might need to be GIT-aware in ways that a human doesn't.
  - ampdepolymerase 6y ago
    That's where ML comes in, to provide the 'intuition' for pruning the search space.
  - jackfoxy 6y ago
    As a human this explanation is emotionally satisfying. It appeals to my sense of human exceptionalism. However how many true but unprovable theorems do we know about? Has anyone ever bothered to compile a list of true but unprovable under the axioms xyz? I would think it is exceedingly hard to manage such research as every axiom set xyz would require companion axioms abc to be provable, and such theorems (at least the non-trivial interesting ones) are possibly hard to reach. This intuition for unprovableness may just be a mechanism for escaping local minima that gets lucky often enough.
juped 6y ago
Math is and has always been a form of expressive art, but there's been a vocal constituency since at least the early 20c that claims it's bloodless symbol manipulation. Since computers excel at bloodless symbol manipulation, one would expect them to be programmable to generate proofs of propositions; this is uninteresting to mathematicians unless it has some artistic merit.
- cthonicthulu 6y ago
  This is a take that I generally agree with. To be honest, I kinda feel the same way about breathless think-pieces talking about GPT-3.
- orange3xchicken 6y ago
  Many mathematicians would disagree with the claim that automated proof checking/generation (see COQ & this presentation by Voevodsky: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins) and involved techniques (see the entire field of sat & smt solvers) are "uninteresting & without artistic merit".
  - juped 6y ago
    Good thing I never claimed that, I just said it was uninteresting to mathematicians unless it has artistic merit!
ur-whale 6y ago
“They’re very controversial for mathematicians,” DeDeo said. “Most of them don’t like the idea.” I've always found this attitude very weird. If I was a miner, I'd welcome the arrival of a machine that helps me dig faster. Even if I was an artist, musician, painter or otherwise working in a "creative" field, I would welcome any kind of tool that helps liberate me from the tedium of material things related to my craft and allow me to reach out further and wider. I think there's a category of Mathematicians that still believe that their craft is something special, and that the help of machines will somehow taint the "purity" of the work. What a sad and arrogant thing to believe.
- ironSkillet 6y ago
  The article touches on it a little bit, but I think the main reason mathematicians are hesitant to accept the value of machines is that although they generate a "proof" in the technical sense, they usually don't generate "understanding", which is really the currency of mathematicians. What good is a proof if literally no human being can understand it? It won't lead to any new mathematics, or new conjectures to think about etc.
  - mherrmann 6y ago
    > What good is a proof if literally no human being can understand it? It establishes the universal truth of a statement. So we absolutely do learn something. Until you have a proof, the statement might also be false.
    - kd0amg 6y ago
      Just knowing something is true without knowing why is a lot less helpful in figuring out what else is true.
      - wisnesky 6y ago
        You are right that computer generated proofs are often tough to understand, and that understanding is often the intended goal of writing a proof. But proofs can be useful for reasons besides human understanding, especially so in engineering. For example, when a browser establishes a secure session with an encryption protocol, the reason it is secure has to do with the difficulty of finding a proof that eg certain numbers factor, but no human cares about this proof. As another example, a compiler can use a proof that a program is type correct to optimize it, but humans would not find such proofs interesting at all.
lixtra 6y ago
Definitions and theorems to prove are (in some sense) more interesting than the proof of a given theorem.
- bunje 6y ago
  Yes, I agree. As a mathematician, I spend lots of time trying to find the correct definitions with only a rough idea what I'm trying to prove (the theorem).
  - orange3xchicken 6y ago
    Conversely, in theoretical cs, there are many longstanding open problems. People who make progress on these problems are taken seriously and listened to precisely because they have new techniques and novel approaches that have not been considered previously - i.e. the theorems & definitions are well understood, but the proofs are the significant element.
ur-whale 6y ago
"If computer scientists are ever able to program a kind of synthetic intuition, he says, it still won’t rival that of humans. " Famous last words, rather similar to the initial comments made by Lee Sedol before starting his famous game against AlphaGo. I don't think machine will ever replace mathematicians. However, I'm ready to bet that most Mathematicians in the coming 50 years who discovers anything useful will do so with CAM (computer assisted math) tools, in the same way no one designs any kind of building in 2020 without the help of a computer.
- sukilot 6y ago
  "If computer scientists are ever able to program a kind of synthetic knitting machine, he says, it still won’t rival that of humans. " If computer scientists are ever able to program a kind of running, he says, it still won’t rival that of humans. " It's amazing to see an "expert" saying these things unironically. The only thing impossible for a computer to event rival a human at are things that are judged subjectively by humans. And even in they, computers are winning. Youth today are learning their culture from computer programs and bots, ever more preferring algorithmically or mechanically generated content to real humans.
  - bawolff 6y ago
    So all the important things? As a human, i care mostly about the things that i subjectively judge good. Pretty much by definition.
- cmehdy 6y ago
  Your assessment seems fair to me. Computers and humans aren't in a fight to win at something, they can just reinforce the lacks of the other. What might happen is that we gradually engineer a smaller and smaller comparative gap between computers and humans by ingesting "human-stuff", and thus make it seem like humans become proportionally irrelevant in the system. But after AlphaGo beat the best players at the game, did people entirely stop playing it? No, in fact they started analyzing the moves and trying to extract ways to improve themselves too. And people around the world don't seem to have particularly given up playing Go either. Similarly with Chess, nobody's even thinking for a second that a computer couldn't beat Magnus consistently, yet we didn't throw our hands in the air and move on from Chess altogether. Maths is not just this abstract thing that some people do, it's something people actively enjoy. If we get computers to stump everyone by bringing something forward that "works" yet we can't grasp, it will only spark more interest in the field. Not everyone is willing to adapt to that attitude if they don't have it yet though.
dnautics 6y ago
Here's what I forsee. GPT3 (or the like) learns strategies to solve problems in a limited DSL (like isabelle). Prompt GPT3 with a problem (e.g. P = NP). Have it walk down the tree of proof possibilities (possibly using Q-learning), trim incorrect branches, and then out comes a proof. Somewhere in its modestly coherent glossolalia, GPT3 will figure out how to prove something "tough for humans" correct. Nice thing is, you might even be able to paralellize the search using independent agents. Is there anyone working on this? Drop a line.
- serendipityrecs 6y ago
  I ran some experiments with GPT3+proofs. You can read about it here: http://serendipityrecs.com/blog/posts/experiments-with-gpt-3/#experiment-3-writing-proofs http://serendipityrecs.com/blog/posts/experiments-with-gpt-3... I wasn't able to get it to return anything interesting but I also didn't spend a lot of time refining the approach (this was just a series of quick and dirty experiments, ultimately I identified recommendations as a good use case for GPT-3 and started building a product around it.) I think it will be interesting to use GPT-3 in conjunction with existing automated/machine proof techniques. Since GPT-3 doesn't "know" anything, automated proof systems can help the system stay logically consistent.
- sukilot 6y ago
  GPT-3 is approximate remixes of old text. How is that at all relevant to theorem proving, which is a search problem?
  - serendipityrecs 6y ago
    Any proof is also a remix of old text (and often times old ideas too)
some-person 6y ago
I think mathematics is an art as well as a science. For mathematicians it can be very exciting to explore, create, and discover new mathematics and, I think, computers provide a new tool in that exploration. So even though a camera can, for example, create a perfect representation of a sunset, that doesn’t mean paintings are now worthless. Creating a painting of a sunset is more than just reproducing the sunset. In a similar way mathematics is more than just producing a proof. Further, the camera is a now a whole new adventure from an artistic perspective because it is a new mechanism for creating art. Similarly computerized systems provide a whole new adventure in terms of exploring and understanding mathematics. Just as the classic art of creating paintings doesn’t invalidate photography, and photography doesn’t invalidate creating paintings (they are both exciting ways to make art), computerized math systems and classical math are exciting ways that can work together to discover mathematics.

100 points by auggierose 6y ago

It's irresponsible to not mention that a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible, in the sense that we cannot just ask a computer to find a proof or refutation of Goldbach's Conjecture or other "Goldbach-type" statement and have it do any better than a person. In that sense, no, computers will never fully automate mathematical reasoning, because mathematical reasoning cannot be fully automated. What we can automate, and have successfully automated many times over, is proof checking. In that sense, yes, computers have already fully automated mathematical reasoning, because checking proofs is fully formalized and mechanized. I think that what people really ought to be asking for is the ease with which we find new results and communicate them to others. In that sense, computer-aided proofs can be hard to read and so there is much work to be done in making them easier to communicate to humans. Similarly, there is interesting work being done on how to make computer-generated proofs which use extremely-high-level axiom schemata to generate human-like handwaving abstractions. I'm still not sure how I feel about the ATP/ITP terminology used here. ATPs are either of the weak sort that crunch through SAT, graphs, and other complete-but-hard problems, or the strong sort which are impossible. Meanwhile, folks have drifted from "interactive" to "assistant", and talk of "proof assistants" as tools which, like a human, can write down and look at sections of a proof in isolation, but cannot summon complete arbitrary proofs from its own mind. Edit: One edit will be quicker than two replies and I tend to be "posting too fast". The main point is captured well by [0], but they immediately link to [1], the central result, which links to [2], an important corollary. At this point, I'm just going to quote WP: > The first [Gödel] incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. > The second [Gödel] incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency. > Informally, [Tarski's Undefinability] theorem states that arithmetical truth cannot be defined in arithmetic. I recognize that these statements may seem surprising, but they are provable and you should convince yourself of them. I recently reviewed [3] and found it to be a very precise and complete introduction to all of the relevant ideas; there's also GEB if you want something more fun. [0] https://en.wikipedia.org/wiki/Automated_theorem_proving#Decidability_of_the_problem https://en.wikipedia.org/wiki/Automated_theorem_proving#Deci... [1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [2] https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo... [3] https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf https://www.logicmatters.net/resources/pdfs/godelbook/GodelB...

lordnacho 6y ago
> a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible Have you got some links? Sounds very interesting.
- a_humean 6y ago
  He is refering to the late 19th and early 20th century work on the foundations of mathematics amoung mathematicans and philosophers. They attempted to fully formalise mathematics. Serveral approaches and schools in mathematics all hit various paradoxes, often of the same kind, and this ultimately culminated in Godel's incompleteness theorems: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... https://plato.stanford.edu/entries/goedel-incompleteness https://plato.stanford.edu/entries/goedel-incompleteness
- umvi 6y ago
  There's also a thing called "the halting problem" which is related to this. Because without the halting problem you could solve any mathematical proof by simply turning it into a computer program that brute forces the problem domain and calculating whether the the program will terminate or not. Of course, this is impossible.
  - sukilot 6y ago
    That's a bit backwards. The halting problem is a computer-flavored variant of Gödel's work. A very simple part -- it's essentially a computer program that says "The program that produced this string is lying".
bigyikes 6y ago
As someone unfamiliar with the results you describe, why can’t a machine do better than a human? A smart human is better at writing proofs than a dumb one. If we had a highly advanced general artificial intelligence, why couldn’t it generate better results than the smart humans?

ogogmad 6y ago

People bringing up GIT (Goedel's Incompleteness Theorem) don't understand that GIT is a limitation of formal logic which affects human mathematicians as much as computer-based mathematicians. Both humans and computers are forced to work with a recursively enumerable set of axioms when constructing mathematical proofs, and so therefore are bound by the same limitations. Also, if you can check a proof, then you can certainly automatically construct a proof, merely by dove-tailing over all possible proofs and checking whether they're correct and imply the desired conjecture. In other words, using GIT when discussing proof automation is irrelevant.

__MatrixMan__ 6y ago
I agree that GIT limits human provers as much as it limits automated ones, but I don't agree that it's irrelevant to the issue. A human mathematician can lean on intuition in ways that a computer can't. Given a theorem that resists proof, a human might develop a feel for whether it's worth continuing to prove via conventional means or whether the troublesome territory is better approached from a different axiom set. That intuition may be driven by the problematic theorem being one of the true-but-unprovable ones that Godel assures us exists without that cause being apparent to the mathematician. The automated prover, on the other hand, faces a halting problem here. Unless it is given some explicit reason to expect that the target is not attainable, it might try forever. So such a prover might need to be GIT-aware in ways that a human doesn't.
- ampdepolymerase 6y ago
  That's where ML comes in, to provide the 'intuition' for pruning the search space.
- jackfoxy 6y ago
  As a human this explanation is emotionally satisfying. It appeals to my sense of human exceptionalism. However how many true but unprovable theorems do we know about? Has anyone ever bothered to compile a list of true but unprovable under the axioms xyz? I would think it is exceedingly hard to manage such research as every axiom set xyz would require companion axioms abc to be provable, and such theorems (at least the non-trivial interesting ones) are possibly hard to reach. This intuition for unprovableness may just be a mechanism for escaping local minima that gets lucky often enough.

juped 6y ago

Math is and has always been a form of expressive art, but there's been a vocal constituency since at least the early 20c that claims it's bloodless symbol manipulation. Since computers excel at bloodless symbol manipulation, one would expect them to be programmable to generate proofs of propositions; this is uninteresting to mathematicians unless it has some artistic merit.

cthonicthulu 6y ago
This is a take that I generally agree with. To be honest, I kinda feel the same way about breathless think-pieces talking about GPT-3.
orange3xchicken 6y ago
Many mathematicians would disagree with the claim that automated proof checking/generation (see COQ & this presentation by Voevodsky: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins) and involved techniques (see the entire field of sat & smt solvers) are "uninteresting & without artistic merit".
- juped 6y ago
  Good thing I never claimed that, I just said it was uninteresting to mathematicians unless it has artistic merit!

ur-whale 6y ago

“They’re very controversial for mathematicians,” DeDeo said. “Most of them don’t like the idea.” I've always found this attitude very weird. If I was a miner, I'd welcome the arrival of a machine that helps me dig faster. Even if I was an artist, musician, painter or otherwise working in a "creative" field, I would welcome any kind of tool that helps liberate me from the tedium of material things related to my craft and allow me to reach out further and wider. I think there's a category of Mathematicians that still believe that their craft is something special, and that the help of machines will somehow taint the "purity" of the work. What a sad and arrogant thing to believe.

ironSkillet 6y ago
The article touches on it a little bit, but I think the main reason mathematicians are hesitant to accept the value of machines is that although they generate a "proof" in the technical sense, they usually don't generate "understanding", which is really the currency of mathematicians. What good is a proof if literally no human being can understand it? It won't lead to any new mathematics, or new conjectures to think about etc.
- mherrmann 6y ago
  > What good is a proof if literally no human being can understand it? It establishes the universal truth of a statement. So we absolutely do learn something. Until you have a proof, the statement might also be false.
  - kd0amg 6y ago
    Just knowing something is true without knowing why is a lot less helpful in figuring out what else is true.
    - wisnesky 6y ago
      You are right that computer generated proofs are often tough to understand, and that understanding is often the intended goal of writing a proof. But proofs can be useful for reasons besides human understanding, especially so in engineering. For example, when a browser establishes a secure session with an encryption protocol, the reason it is secure has to do with the difficulty of finding a proof that eg certain numbers factor, but no human cares about this proof. As another example, a compiler can use a proof that a program is type correct to optimize it, but humans would not find such proofs interesting at all.

lixtra 6y ago

Definitions and theorems to prove are (in some sense) more interesting than the proof of a given theorem.

bunje 6y ago
Yes, I agree. As a mathematician, I spend lots of time trying to find the correct definitions with only a rough idea what I'm trying to prove (the theorem).
- orange3xchicken 6y ago
  Conversely, in theoretical cs, there are many longstanding open problems. People who make progress on these problems are taken seriously and listened to precisely because they have new techniques and novel approaches that have not been considered previously - i.e. the theorems & definitions are well understood, but the proofs are the significant element.

ur-whale 6y ago

"If computer scientists are ever able to program a kind of synthetic intuition, he says, it still won’t rival that of humans. " Famous last words, rather similar to the initial comments made by Lee Sedol before starting his famous game against AlphaGo. I don't think machine will ever replace mathematicians. However, I'm ready to bet that most Mathematicians in the coming 50 years who discovers anything useful will do so with CAM (computer assisted math) tools, in the same way no one designs any kind of building in 2020 without the help of a computer.

sukilot 6y ago
"If computer scientists are ever able to program a kind of synthetic knitting machine, he says, it still won’t rival that of humans. " If computer scientists are ever able to program a kind of running, he says, it still won’t rival that of humans. " It's amazing to see an "expert" saying these things unironically. The only thing impossible for a computer to event rival a human at are things that are judged subjectively by humans. And even in they, computers are winning. Youth today are learning their culture from computer programs and bots, ever more preferring algorithmically or mechanically generated content to real humans.
- bawolff 6y ago
  So all the important things? As a human, i care mostly about the things that i subjectively judge good. Pretty much by definition.
cmehdy 6y ago
Your assessment seems fair to me. Computers and humans aren't in a fight to win at something, they can just reinforce the lacks of the other. What might happen is that we gradually engineer a smaller and smaller comparative gap between computers and humans by ingesting "human-stuff", and thus make it seem like humans become proportionally irrelevant in the system. But after AlphaGo beat the best players at the game, did people entirely stop playing it? No, in fact they started analyzing the moves and trying to extract ways to improve themselves too. And people around the world don't seem to have particularly given up playing Go either. Similarly with Chess, nobody's even thinking for a second that a computer couldn't beat Magnus consistently, yet we didn't throw our hands in the air and move on from Chess altogether. Maths is not just this abstract thing that some people do, it's something people actively enjoy. If we get computers to stump everyone by bringing something forward that "works" yet we can't grasp, it will only spark more interest in the field. Not everyone is willing to adapt to that attitude if they don't have it yet though.

dnautics 6y ago

Here's what I forsee. GPT3 (or the like) learns strategies to solve problems in a limited DSL (like isabelle). Prompt GPT3 with a problem (e.g. P = NP). Have it walk down the tree of proof possibilities (possibly using Q-learning), trim incorrect branches, and then out comes a proof. Somewhere in its modestly coherent glossolalia, GPT3 will figure out how to prove something "tough for humans" correct. Nice thing is, you might even be able to paralellize the search using independent agents. Is there anyone working on this? Drop a line.

serendipityrecs 6y ago
I ran some experiments with GPT3+proofs. You can read about it here: http://serendipityrecs.com/blog/posts/experiments-with-gpt-3/#experiment-3-writing-proofs http://serendipityrecs.com/blog/posts/experiments-with-gpt-3... I wasn't able to get it to return anything interesting but I also didn't spend a lot of time refining the approach (this was just a series of quick and dirty experiments, ultimately I identified recommendations as a good use case for GPT-3 and started building a product around it.) I think it will be interesting to use GPT-3 in conjunction with existing automated/machine proof techniques. Since GPT-3 doesn't "know" anything, automated proof systems can help the system stay logically consistent.
sukilot 6y ago
GPT-3 is approximate remixes of old text. How is that at all relevant to theorem proving, which is a search problem?
- serendipityrecs 6y ago
  Any proof is also a remix of old text (and often times old ideas too)

some-person 6y ago

I think mathematics is an art as well as a science. For mathematicians it can be very exciting to explore, create, and discover new mathematics and, I think, computers provide a new tool in that exploration. So even though a camera can, for example, create a perfect representation of a sunset, that doesn’t mean paintings are now worthless. Creating a painting of a sunset is more than just reproducing the sunset. In a similar way mathematics is more than just producing a proof. Further, the camera is a now a whole new adventure from an artistic perspective because it is a new mechanism for creating art. Similarly computerized systems provide a whole new adventure in terms of exploring and understanding mathematics. Just as the classic art of creating paintings doesn’t invalidate photography, and photography doesn’t invalidate creating paintings (they are both exciting ways to make art), computerized math systems and classical math are exciting ways that can work together to discover mathematics.