[HN Gopher] HOList: An Environment for Machine Learning of Highe...
       ___________________________________________________________________
        
       HOList: An Environment for Machine Learning of Higher-Order Theorem
       Proving (2019)
        
       Author : mathematically
       Score  : 11 points
       Date   : 2021-09-22 17:30 UTC (5 hours ago)
        
 (HTM) web link (arxiv.org)
 (TXT) w3m dump (arxiv.org)
        
       | Y_Y wrote:
       | (2019)
       | 
       | 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.
        
         | miloignis wrote:
         | Automation of boring theorems for software properties /
         | correctness would be very useful, even if it didn't produce new
         | mathematical results!
        
       | [deleted]
        
       ___________________________________________________________________
       (page generated 2021-09-22 23:03 UTC)