Proofs in Mathematica

Most of the individual built-in functions of Mathematica I designed to be as predictable as possible—applying transformations in definite ways and using algorithms that are never of fundamentally unknown difficulty. But as their names suggest Simplify and FullSimplify were intended to be less predictable—and just to do what they can and then return a result. And in many cases these functions end up trying to prove theorems; so for example FullSimplify[(a + b)/2 ≥ Sqrt[a b], a > 0 && b > 0] must in effect prove a theorem to get the result True.