This looks pretty interesting! is a theorem prover based on homotopy type theory, with IDE support for IntelliJ:
Conversation
There's an announcement post here for those interested: groups.google.com/forum/#!topic/ - gives a bit more background into why is working on it!
2
1
Seems like it's mainly there to explore how modern IDEs could be used for theorem proving, which I think is a great goal! Would be cool to see more creators of dependently typed programming languages looking beyond Emacs, to supporting things like the Language Server Protocol.
2
6
Oh wow, it seems they have a whole research group working on it: research.jetbrains.org/groups/group-f
1
1
Interesting indeed! I approve of the continuing tradition of naming proof assistants after birds.
2
1
3
Ah, “eagle”, surprised I didn’t pick up on that!
If I ever make a similar thing, I ought to call it “erne” (the Old English word of the same origin)
1