Cheers. That's way much more information than I ever wanted to know about that sorry affair. If it can quell the torrent of ad-hominems, it's worth it, but I doubt it. All those hardcore soft. engineers here on HN who spend 99.99999% of uptime close to the bare metal think that people like Gebru who work on ethics are useless hangers-on without any "real contributions" (probably because none of them has bothered to check her background on wikipedia).
Nevertheless, hoping to check your sources I clicked through your profile and I have a question, totally unrelated to all this. Can you say something about the state of the art in "neural proof synthesis"? To clarify, I'm scare-quoting because I didn't even know that's a thing. For context, my background is in the European tradition of Resolution-based automated theorem proving (Prolog and all that) but also statistical machine learning, so don't worry about simplifying terminology too much.
Btw, the "proof engineering" link in your profile gives me a security alert on firefox.
Nevertheless, hoping to check your sources I clicked through your profile and I have a question, totally unrelated to all this. Can you say something about the state of the art in "neural proof synthesis"? To clarify, I'm scare-quoting because I didn't even know that's a thing. For context, my background is in the European tradition of Resolution-based automated theorem proving (Prolog and all that) but also statistical machine learning, so don't worry about simplifying terminology too much.
Btw, the "proof engineering" link in your profile gives me a security alert on firefox.