g `~(?n. !p. prime p ==> p <= n)` ;; e( STRIP_TAC THEN ABBREV_TAC `k = FACT n + 1` );; e( SUBGOAL_THEN `?p. prime p /\ p divides k` MP_TAC );; e( ASM_MESON_TAC [FACT_LE; ARITH_RULE `1 <= f ==> ~(f + 1 = 1)`; PRIME_FACTOR] );; e( STRIP_TAC …

miz3 http://arxiv.org/abs/1201.3601 はメモリー（Unixのみ）に常駐して mizar のような natural language declarative style の証明を書く為の自動入力ツールで，インストールは cp miz3/exrc ~/.exrc export PATH = $PATH:~/CAS/hol_light/miz3/bin とし…