【１】Mathematicaによる証明

　まず，

　　算術平均の幾何平均≧幾何平均の算術平均

の不等式から始めたい．２０年ほど前のことだが，３変数の算術平均の幾何平均≧幾何平均の算術平均の不等式

　　（ａ^2＋ｂ^2）（ｂ^2＋ｃ^2）（ｃ^2＋ａ^2）／２^3≧（ａｂ＋ｂｃ＋ｃａ）^3／３^3

を調べたところ，素直に計算してくれてtrueを返してきた．Mathematicaが計算してくれた部分の証明は不明であるが，便利なパッケージがあってそれが結構使えることに感嘆するのみである．

　しかし，４変数版

　　（ａ^2＋ｂ^2＋ｃ^2）（ａ^2＋ｂ^2＋ｄ^2）（ａ^2＋ｃ^2＋ｄ^2）（ｂ^2＋ｃ^2＋ｄ^2）／３^4≧（ａｂｃ＋ａｂｄ＋ａｃｄ＋ｂｃｄ）^4／４^4

は数時間たっても計算が終わらず，その後，徹夜稼働で結果を待ったが，システムのメモリーを使い果たしエラー終了となったそうだ．コンピュータは残念ながら不調であったが，人間ならば３変数でも４変数でもヘルダーの不等式を使ってうまい証明を与えることができるのだが，・・・．

　このような不等式をコンピュータに自動証明させるためには，前提となる基本定理が与えられていればコンピュータは自分の目的に都合のよいように変形しうまくあてはめて証明に至るはずである．このような試みは人工知能研究の有力な分野として古くから研究されているのだが，コンピュータも往々にして失敗する．まだまだ人間のように融通がきかないということだろう．

＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝