Graph Representations for Higher-Order Logic and Theorem Proving

arxiv.org

24 points·mwakanosya··6 comments

The title here Deep learning can now prove half of what expert mathematicians can misrepresents and overstates the conclusions and claims made by the actual paper.

The title appears to derive from the single sentence "Our best model automatically proves 48% of the theorems in the validation set."

Agreed. We changed it to the title of the paper.

This looks to be a serious work that has been given a title by a corrupt gonzo science journalist!

The actual work looks to be about converting existing proofs to a formalised graph based encoding (using ml)

From the earlier cited paper, this seems to target relatively simple proofs too (i.e., hardly what "expert mathematicians can prove"): "... a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture."

IMO formal theorem proving is the future of mathematics for sure. I've been working on Metamath a bit and basically proving a new theorem reduces to a search problem over the theorems already proven.

In 10 years I think every mathematician will use formal methods, it will be like typing your proofs with a type writer not to. Moreover the problems are very amenable to smart tools assisting in the work, there is a smooth path from where we are now to a fully ai mathematician.

Agree with the others here that the title is not accurate or representative of the conclusions of this paper.

“In the experiments presented in this paper, we predict tactics and their arguments by looking only at the conclusion of the current sub-goal and ignoring any local assumptions that could be crucial to the proof. This is a serious limitation for our system, and in future work we would like to include the local assumptions list when generating the embedding of the goal.”

Reply on news.ycombinator.com