形式化された定理の証明では．．．

適当な tactics を用いて論理記号を外し，atomic formula に分解する作業にそれほどの困難はありません．問題は，そのあと，定数，変数，関数，述語記号などからなる式を「計算」により証明する部分にあります．

実際，各種の「検証」で高名な HOL4 も他の証明系と同じく，有理数以降の代数処理はかなり窮屈で，例えば

val POW_3 = METIS_PROVE [pow,POW_1,REAL_MUL_ASSOC,ARITH_CONV``3=SUC(SUC 1)``]``!x:real. x pow 3=x*x*x``;

METIS_PROVE [
SIMP_CONV (real_ss ++ REAL_ARITH_ss) [POW_3] ``!a b c:real. (a pow 3+b pow 3+c pow 3=3*a*b*c)<=>((a+b+c)*(a*a+b*b+c*c-a*b-b*c-c*a)=0)``,
SIMP_CONV (real_ss ++ REAL_ARITH_ss) [REAL_ENTIRE] ``!a b c:real. ((a+b+c)*(a*a+b*b+c*c-a*b-b*c-c*a)=0)<=>(a+b+c=0:real)\/((a-b)*(a-b)+(b-c)*(b-c)+(c-a)*(c-a)=0)``,
METIS_PROVE [REAL_LE_SQUARE, REAL_LE_LT, REAL_POS_NZ, REAL_LET_ADD, REAL_LTE_ADD, REAL_LT_ADD, REAL_LE_ADD, REAL_ADD_RID, REAL_SUB_0, REAL_MUL_RZERO, REAL_ENTIRE] ``!a b c:real. ((a-b)*(a-b)+(b-c)*(b-c)+(c-a)*(c-a)=0)<=>(a=b)/\(b=c)/\(c=a)``
]``!a b c:real. (a+b+c=0)\/(a=b)/\(b=c)/\(c=a) <=> (a pow 3+b pow 3+c pow 3=3*a*b*c)``;
r[+0+7]+0+0+1+2+2+0+1+0+5#
> val POW_3 =
     [] |- ∀x. x pow 3 = x * x * x
     : thm
- metis: r[+0+20]+1+1+0+0+0+0+0+0+0+0+0+0+0#
r[+0+18]+0+0+0+0+0+0+0+0+0+0+0+0+0+2+0+2+0+2+3+3+2+2+1+3+0+2+1+2+1+1+1+1#
r[+0+18]+0+0+0+0+0+0+0+0+0+0+0+0+0+0+2+0+2+2+4+3+2+2+1+1+1+2+0+0+1+1#
r[+0+18]+0+0+0+0+0+0+0+0+0+0+0+0+0+2+0+2+2+0+3+3+2+2+1+1#
metis: r[+0+13]+0+0+0+0+0+0+0+0+4+14+18r+9+18+6+17r+7+15r+15+1+5+15r+15+4+0+0+8+0+15r+1#
r[+0+14]+1+1+0+0+0+0+0+0+4+6+16+19r+12+14+15r+15r+2#
r[+0+12]+0+0+0+0+0+0+0+4+14+6+15r+23+1#
> val it =
     []
    |- ∀a b c.
         (a + b + c = 0) ∨ (a = b) ∧ (b = c) ∧ (c = a) ⇔
         (a pow 3 + b pow 3 + c pow 3 = 3 * a * b * c)
     : thm

のように手間が掛かります．

ところが，HOL Light は，何と申しますか証明系にあるまじき強力な代数proverを備えおり，同じ定理もご覧の通りです．

# MESON
  [REAL_SOS`a pow 3+b pow 3+c pow 3= &3*a*b*c <=> a+b+c= &0 \/ (a-b) pow 2+(b-c) pow 2+(c-a) pow 2= &0`;
   REAL_SOS`(a-b) pow 2+(b-c) pow 2+(c-a) pow 2= &0<=>a=b /\ b=c /\ c=a`]
  `!a b c:real. a+b+c= &0 \/ a=b /\ b=c /\ c=a <=> a pow 3+b pow 3+c pow 3= &3*a*b*c` ;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
0..0..1..solved at 5
0..0..1..7..30..119..solved at 183
0..0..2..10..42..solved at 93
0..0..2..10..42..solved at 76
0..0..2..10..42..solved at 59
val it : thm =
  |- !a b c.
         a + b + c = &0 \/ a = b /\ b = c /\ c = a <=>
         a pow 3 + b pow 3 + c pow 3 = &3 * a * b * c