Hacker News new | past | comments | ask | show | jobs | submit login
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (2019) (arxiv.org)
13 points by mathematically 31 days ago | hide | past | favorite | 3 comments


I'd be delighted to see "deep learning" produce a non-trivial breakthrough, but it feels like theorem proving must be about as hard as it gets for just learning a heuristic from piles of examples.

In particular, it's very easy to prove boring theorems, very hard to prove outstanding conjectures, and downright impossible to work out which theorems will turn out to be interesting.

Automation of boring theorems for software properties / correctness would be very useful, even if it didn't produce new mathematical results!

I would like a thing where I put in a proposition and attempts are made at autocomplete style proofs of the proposition. Maybe you can do that with program synthesis techniques and Lean style theorem provers.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact