Imogen is a theorem prover for intuitionistic propositional logic, written with my advisor Frank Pfenning. We plan for the next major release of Imogen to support first-order intuitionistic logic in addition to the specialized propositional prover.