<\body> Some people which are not part of the core development team use for other projects. We do our best to support such external developments and make the necessary changes inside when necessary. Here follows a list of a few initiatives that we have been aware of: <\itemize> Lionel Mamane has developed a plug-in for the |https://coq.inria.fr/> proof assistant, called , but was never released publicly. Similarly, Henri Lesourd developed an interface to the \mega mathematical assistant system. The use of as a front-end for proof assistants and theorem provers raises interesting questions about asynchroneous plug-in evaluations, keeping track and appropriate rendering of the state of a prover, appropriate mathematical and proof markup, etc. Saugata Basu, Richard Pollack and Marie-Fran�ois Roy have written an interactive book \P\Q using . Any people interested in developing addional interactive features inside are invited to contact us. and formerly have considered developing a for . Another such initiative is |http://www.nongnu.org/fangle/>, which has recently been started by . Any concrete implementation of their proposals would happily find its way into the main distribution. If you want to start a project based on , then please let us know. >