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
This Tweet was deleted by the Tweet author. Learn more
Yeah, it’s one of the reasons I get more use out of Lean than Agda or Coq.