<\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 are aware of: <\itemize> is developing a plug-in for the |http://coq.inria.fr/coq-fra.html> proof assistant, called . A first version of this plug-in is about to be released; please check Lionel's homepage. Similarly, Henri Lesourd is developing an interface to the . 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 ``'' 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. <\initial> <\collection>