Isabelle/Isar: A Practical Approach

　定理証明システムは巷で言われるようなプログラムや約款？の検証ツールではなく，あくまで計算機上に数学の理論を公理論的に構成する為のものです．
　しかしながら，数学の人間はこうしたソフトをあまり（というか全く）利用していないのが現状であり，その理由として

・存在を知らない
・計算機上に数学を構成することに興味がない，時間がない
・計算機が苦手
・殆どのマニュアルの例はロジックやリストばかり
・ロジックが嫌い
・殆どのシステムは計算が出来ない

などが挙げられます．こうした状況に一石を投じるべく（失笑）相加平均と相乗平均との大小関係の証明を例に"Isabelle/Isar: A Practical Approach"を書いていこうと思います．