HOL(y) Hammer

リモートが動かなくなったと思っていたら，オンラインのインターフェイスが公開されていました．例えば，．．．

g `!n. &1 + &n <= &2 pow n` ;;

の証明スクリプト．人（私）が書くと

e( INDUCT_TAC THEN REWRITE_TAC [REAL;pow] THEN ASM_ARITH_TAC );;

といった感じですが，http://colo12-c703.uibk.ac.at/hh/ は

e( MESON_TAC[REAL_OF_NUM_POW;REAL_OF_NUM_LE;REAL_OF_NUM_ADD;NUMERAL;LT_POW2_REFL;LE_SUC_LT;ADD_SYM;ADD1] );;

と答えます．でも実は

# LT_POW2_REFL;;
val it : thm = |- !n. n < 2 EXP n

なので．．．