4 ms·

I wonder if it's possible for an machine learning algorithm to simplify these proofs. I take it because of the rather strict domain specificness of math papers

by tinco 14y ago

I wonder if it's possible for an machine learning algorithm to simplify these proofs. I take it because of the rather strict domain specificness of math papers it should be possible to develop an algorithm that can parse these papers into lemmas. Proofs normally structured as a tree of lemmas right? Or are there proofs that have more complex structure? A single basic thing could be to extract the leaf lemmas and assert their validity. If they are valid, and the relations between the lemmas are valid then the eventual conclusion should also be valid. Has anything like this ever been attempted? A math paper proof verifying machine learning algorithm?

jlouis 14y ago
Automated Therom Proving is ridiculously hard and a guess would be that it is almost impossible to train an ML algorithm to do this efficiently. However, verifying that a proof is correct is somewhat simple, if you give the machine enough information to actually run the formalization details. In modern mathematics, this may be a necessary thing to do since nobody has time to verify these 1000 page developments anymore. The problem is that the level of detail currently needed is very high. And this slows down the formalization process. But the area is in wild development these years, so hopefully something good comes out of it.
- jamesaguilar 14y ago
  Just imagine inputting the final character of the last inference step, then waiting for a few minutes while the computer performs incremental compilation of the last few rules. Finally, it emits simply these four characters: "QED."
  - dandrews 14y ago
    I like this, and it reminds me of the tagline from Asimov's The Last Question.
    - sp332 14y ago
      There was a billionaire in the book Permutation City who uploaded his brain into a supercomputer, then let an optimizer run on it for years. The goal was to get his brain to run in real-time or better, but eventually it spit out an empty file and a log message: "This program produces no output."
- raverbashing 14y ago
  Yes Still, I think it would be better if mathematicians started writing their theorems and proofs in a machine readable way Of course there is no standart for that today that gets "everything". Something "let G be a Galois Group, let Xk be the set of all matrixes of dimension k,k where Det(x)=1" etc This is hard. But to put it in that way would allow for piecewise revision, reassembly, study and proof (not that you can't do that on paper, but it's much harder), and then you can start growing your machine programs around those proofs.
  - ColinWright 14y ago
    : I think it would be better if mathematicians : started writing their theorems and proofs in : a machine readable way And software would be more reliable if people used the correctness-proving systems that have been developed.
    - raverbashing 14y ago
      "Beware of bugs in the above code; I have only proved it correct, not tried it." Donald Knuth
      - ColinWright 14y ago
        So, you're saying that the code would be less reliable if there was no work to prove it formally? Of course you aren't. What you're saying is that proving code is correct is insufficient. Of course it is insufficient. Your comment adds nothing to the debate. What I'm saying is that asking that mathematicians produce their proofs in a form amenable to mechanical checking is like asking programmers to produce their code in a form that is amenable to mechanical checking. It's long, tedious, error-prone in its own right, and simply not going to happen. It's like asking people who write multi-million line programs in high-level languages to get the same functionality by writing in assembler. Programming doesn't happen like that, and proofs don't either.
        raverbashing 14y ago
nairboon 14y ago
There are numerous projects for proof checking: https://en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking Such an algorithm could consist of the following parts: * a parser * a syntax checker: to test how correct the used mathematical notation is * if possible translate non-standard notation to standard * using some sort of supervised learning for checking existing proofs with existing proof solvers * manual intervention: improve translator or underlying proof solver

by tinco 14y ago

jlouis 14y ago

Automated Therom Proving is ridiculously hard and a guess would be that it is almost impossible to train an ML algorithm to do this efficiently. However, verifying that a proof is correct is somewhat simple, if you give the machine enough information to actually run the formalization details. In modern mathematics, this may be a necessary thing to do since nobody has time to verify these 1000 page developments anymore. The problem is that the level of detail currently needed is very high. And this slows down the formalization process. But the area is in wild development these years, so hopefully something good comes out of it.

jamesaguilar 14y ago
Just imagine inputting the final character of the last inference step, then waiting for a few minutes while the computer performs incremental compilation of the last few rules. Finally, it emits simply these four characters: "QED."
- dandrews 14y ago
  I like this, and it reminds me of the tagline from Asimov's The Last Question.
  - sp332 14y ago
    There was a billionaire in the book Permutation City who uploaded his brain into a supercomputer, then let an optimizer run on it for years. The goal was to get his brain to run in real-time or better, but eventually it spit out an empty file and a log message: "This program produces no output."
raverbashing 14y ago
Yes Still, I think it would be better if mathematicians started writing their theorems and proofs in a machine readable way Of course there is no standart for that today that gets "everything". Something "let G be a Galois Group, let Xk be the set of all matrixes of dimension k,k where Det(x)=1" etc This is hard. But to put it in that way would allow for piecewise revision, reassembly, study and proof (not that you can't do that on paper, but it's much harder), and then you can start growing your machine programs around those proofs.
- ColinWright 14y ago
  : I think it would be better if mathematicians : started writing their theorems and proofs in : a machine readable way And software would be more reliable if people used the correctness-proving systems that have been developed.
  - raverbashing 14y ago
    "Beware of bugs in the above code; I have only proved it correct, not tried it." Donald Knuth
    - ColinWright 14y ago
      So, you're saying that the code would be less reliable if there was no work to prove it formally? Of course you aren't. What you're saying is that proving code is correct is insufficient. Of course it is insufficient. Your comment adds nothing to the debate. What I'm saying is that asking that mathematicians produce their proofs in a form amenable to mechanical checking is like asking programmers to produce their code in a form that is amenable to mechanical checking. It's long, tedious, error-prone in its own right, and simply not going to happen. It's like asking people who write multi-million line programs in high-level languages to get the same functionality by writing in assembler. Programming doesn't happen like that, and proofs don't either.
      - raverbashing 14y ago

nairboon 14y ago

There are numerous projects for proof checking: https://en.wikipedia.org/wiki/Automated_proof_checking https://en.wikipedia.org/wiki/Automated_proof_checking Such an algorithm could consist of the following parts: * a parser * a syntax checker: to test how correct the used mathematical notation is * if possible translate non-standard notation to standard * using some sort of supervised learning for checking existing proofs with existing proof solvers * manual intervention: improve translator or underlying proof solver