4 ms·
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, verif
by 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 agoJust 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 agoI like this, and it reminds me of the tagline from Asimov's The Last Question.
- sp332 14y agoThere 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 agoYes 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 agoSo, 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 agoAnd your comment adds nothing to the debate while picking on a joke. "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" But programs are done in a form that's subject to mechanical checking. Compilers do that and only compile code that adheres to a strict syntax and grammar. In a higher level there are static code analysers that look for other defects. Some of them are in compilers already for optimization purposes. Also, semiconductor companies use automated checkers for the inner parts of their processors, like floating point multipliers to make sure they are correct.