Use Coq in the Browser: The JsCoq Theorem Prover Online IDE

JsCoq is an interactive, web-based environment for the Coq Theorem prover, developed at the Centre de Recherche en Informatique of MINES ParisTech (former École de Mines de Paris). We don’t provide a Coq tutorial (yet), but as a showcase, we display a proof of the infinitude of primes in Coq. The proof relies in the Mathematical Components library by the MSR/Inria team led by Georges Gonthier, so our first step will be to load it and set a few Coq options:

Source: jscoq.github.io