I'm curious how they arrived on some of these topics: Things like proof assistants seem like relatively straightforward extensions of their programming language expertise, but paper summarisation seems really out of left field.

It also says it's a private entity--is this structured as a pure research company owned by JetBrains or as something else?

Cool my IntelliJ license is (maybe?) supporting some really interesting academic projects.