[YeGoblynQueenne]

Thanks. I'm a bit more familiar with neural theorem proving. It's an interesting area. For example, if I could train me a model to speed up (NP-complete) θ-subsumption for very long terms that would be a worthy addition to the purely symbolic toolbox I'm more at home with.

Autoformalization also sounds interesting. I've had some conversations about automatically turning big corpora of natural language text into Prolog with language models, for example. I don't reckon anyone is even researching how to do this with symbolic methods at the moment.

I'll check out AITP. Thanks for the pointers. I'm used to small conferences [and to underciting between disciplines] :)

[tlringer]

I went to AITP for the first time last September, and I found it an absolute pleasure. Everyone was kind and wonderful and open-minded. The venue was wonderful too. Highly recommended if you're interested at any point.

[YeGoblynQueenne]

And the next one is easy to get to by train from my current location. That's great (I don't fly). Nice.

[tlringer]

Hopefully I'll see you there!

BTW what you say about the sadly common assumption Timnit and other AI ethics folks don't have "real contributions" is too real. It has impacted me even though my work isn't on AI ethics at all, just because I bother to talk about it online in public sometimes. Similarly for any social justice work or any work improving the work environment in research. It is like some people cannot comprehend that one can be technically proficient and still care about social justice and ethics and other "soft" issues. I love how confused those people are when they learn my expertise is in formal logic and proof haha

[YeGoblynQueenne]

It's lack of training I think. A good engineer should think about the consequences of her actions. People in the industry, it seems, just don't. Very disappointing.