Globular is a new proof assistant in which a proof is represented as a
geometrical object, in principle in any dimension. Our interface
radically rejects the standard text-based input paradigm, with all
user interaction via the mouse; as users click and drag parts of their
object, they incrementally change its structure, and in this way build
their proof. In this way, the software more closely resembles a
computer drawing package than a traditional proof assistant. Globular
is also web-based, to lower barriers to entry; perhaps as a result,
community takeup as been strong, with the software being used 19,000
times by 4,000 users since launch in December 2015. In this talk I
will focus on the design challenges we faced in developing our proof
assistant, and ask the community for advice in tacking the further
design hurdles we face as the proof assistant is developed.