[Ericson2314]

I've always been a bit of an A.I. skeptic/grinch, but there are things to very much like here.

Firstly, is an idea that we've deeper learned ML quite a lot, and we need more representations / abstract thinking again to make more fundamental progress. Nice, I like the sound of that.

Secondly,

> ... So Christian Szegedy and Sarah Loos have the system where you take sort of a regular theorem prover and you give it a problem. And then you have a neural net decide out of the million axioms I have, which 100 are most relevant to this problem. ...

I also thought combining machine learning with theorem provers would be an excellent avenue for further research: we have abstract reasoning that doesn't "go wrong" as it does in many end applications ("expert systems don't work"), but is also still extremely "rich", and not trivially automated because it's intractable without intuition/heuristics.

Glad to hear the big leagers are also interested.

[mountainriver]

It seems like theorem provers are where all the action should be, but oddly isn’t