A nice picture, too bad!

The PhoX Proof Assistant

Beware: work in progress.

Current version is 0.89.170316

PhoX is a proof assistant based on High Order logic and it is eXtensible. One of the principle of this proof assistant is to be as user friendly as possible and so to need a minimal learning time. The current version is still expirimental but starts to be really usable. It is a good idea to try it and make comments to improve the final version.

Hot news


  • An overview
  • Documentation
  • Examples
  • The team
  • The distribution
  • Exercises for math students formalized on computers (not only with Phox)

  • PhoX overview

    The major design goal of this program was to make as easy as possible the formalization of mathematical proofs on machine. This is quite a hard goal to reach. For instance, if you consider knots theory, you will have great problems to translate your graphical proofs !

    However, I have put a lot of work to make it possible to formalize a lot of mathematics quite easily. Here are a list of the features offered by this program (quite a few of them are unique!):



    Here is a very simple proof development: a proof of the existence of the quotient and remaining of the euclidain division. You can browse

    The team

    All people working on PhoX are member of the Laboratory of Mathematic of the Savoy University or the Logic Team of Paris VII university. Although some part of the code where written while C. Raffalli was at L.F.C.S. in Edinburgh or at Chalmers university.

    Christophe Raffalli
    Author of most of the implementation.
    Philippe Curmin
    P. Curmin is working on a marking algorithm to optimise extracted programs. This work should be useful in future versions.
    Pascal Manoury
    P. Manoury may port in the future the ProPre system within PhoX. This should allow a lot of totality proofs to be automatized (proof that a given equational definition of a function always terminates)
    Paul Roziere
    P. Roziere formalized quite a few proofs in the system and is responsible for most of the emacs mode.

    PhoX distribution (0.89)

    Christophe Raffalli /LAMA, Savoie University / raffalli@univ-savoie.fr
    Last modified: Tue Mar 1 17:30:58 CET 2005