Mymms Interactive
Demo

Mymms is a project of computer algebra system based upon a proof assistant.

Local archive: mymms-0.0.1.tgz

Poussin Interactive
Demo

examples (to copy and paste):
simple examplematrices (dependent type)

First Coq challenge ;)

Definition of peano numbers + proof for decidability of equality

Minima Interactive
Demo