Well, there's a new batch of autoformalization attempts with LLMs now. Although I've also heard people say autoformalization will always be impossible.

It's interesting to wonder what kind of coverage Cycorp managed to achieve internally, and on what domains. Seemingly no job openings at the moment though!