随分と以前から、「証明はアニメーションなんだ」と言ってます。このことを認識してないと、さほど難しくもないことが無闇と難しいモノになってしまうと思うんですよ。
この記事では具体的な事例を出してないので、モンヤリした話ですが、たぶん、具体的な事例を出す機会はあると思うので書いておきます。
アニメーションと、代替の表現手段
「証明はアニメーション」は、比喩とか例え話ではなくて、「実際にそうだよ」ってことです。なので、まず通常の「アニメーション」について語ります。が、僕がアニメ好きとか詳しいとか、では全くありません。非常に基本的な概念を確認するだけです。
現在の娯楽、あるいは芸術作品として公開されているアニメは、1秒に24フレーム（以上）らしいです。10秒で240フレームですね。素人作品で、多少粗い動きでもいいや、って事なら8フレーム/秒とかでもいいかも知れません。
いま、アニメを作りたい人がいたとします。しかし、作るための機材（ツール）もなく、技術も知識もないとします。でもなにか作りたい！ さぁ、どうしましょう？ いくつかの選択肢があります。
- パラパラ漫画にする。
- 紙芝居にする。
- マンガにする。
- 小説にする。
パラパラ漫画は、フィルム（デジタルなモノも含めてフィルムと呼ぶ）の代わりに、複数枚の紙を使いますが、原理はアニメーションと同じと言っていいでしょう。フレームレートは … よく分かりませんが、仮に10フレーム/秒としておきましょう。10秒で100枚の紙が必要です。
紙芝居は、表現手段としてパラパラ漫画とは違うものです。フレームレート(？)が10秒で1枚とかでしょう。絵の動きは最早なくて、代わりに「語り」を使います。
マンガもまた表現手段として別なものになります。パラパラ漫画として描いた絵達を、台紙に順番に貼り付けていったらマンガになるでしょうか？ それはマンガではなくて、一連の動きのスナップショット群を一度に見せただけです。マンガにはマンガとしての語彙・文法があります（「記法バイアスと記法独立な把握： 順序随伴を例として // 語彙、文法、記法」参照）
小説になると、非常に異なった表現手段になるので、別な才能が必要になります。アニメーションで伝えたかったことが、はたして小説で伝わるのかも疑問です。
アニメーション作成ツールとしての証明支援系
「証明はアニメーションなんだ」の意味は、証明が、ある種の絵〈図形〉が変化していく様を見せるものだからです。ストーリーの分岐や合流もあります。人間は同時に複数のストーリーを追うのは難しいので、メイン・ストーリーのあいだにサイド・ストーリーを適宜挟むとかして分岐・合流を表すことになるでしょう。
この事を考えれば、証明作成支援ツール〈証明支援系〉は、アニメーション作成ツールと似たものになるでしょう。僕がGlobularを高く評価するのは、（現状の出来ばえはともかくとして）アニメーション作成ツールの方向に一歩進めた（おそらくは初めての）ソフトウェアだからです。（もし、Globularに興味が湧いたなら「Globularの使い方 (1)」をどうぞ。）
Globularは、フレーム群に相当する複数の絵（静止画）を作成するお絵描き機能を持っています。同時に、複数の絵達が関連して持つ構造も指定できます。再生〈リプレイ〉をどうするかを制御する機能は（今は）なくて、ユーザー側が好きに探索するようになっています。その意味では、ゲームの舞台（例えばダンジョン）だけを作成するツールのようでもあります。時間方向のストーリーが特になくても、舞台内を勝手に動き回って探索できれば、けっこう面白いです。
Globularは、背景としている原理も新しいのですが、伝統的な論理に基づく証明支援系であっても、要求される機能は同じです。フレームに相当する静止画の作成機能、フレームどうしの関連を指定する構造化の機能です。
ストーリーには分岐や合流がありますが、制作者側が再生手順を完全に決めるのではなくて、ユーザー（作品の視聴者）が対話的に選択できるようにするほうが望ましいでしょう。証明という作品は、受動視聴には向いてないので、早送り・巻き戻しのような、いやもっと高機能なナビゲーションが必須です。
劣悪な制作環境・視聴環境
アニメーション作品としての証明を制作する環境は、まったく整っていません。アニメーション作品としての証明を再生・視聴する環境もありません。これは、デジタルなツールだけの話ではなくて、紙媒体においても事情は同様です。
「いや、TeXで綺麗に組版できるじゃないか」 -- そういう話ではありません。アニメーションを諦めるにしても、代替表現手段もロクなもんがないのです。
アニメーションがダメなら、まずはパラパラ漫画でしょう。時間に沿った再生（パラパラすること）が難しいなら、台紙に貼って見せることになります*1。僕は、この「台紙に貼ったパラパラ漫画」はありだと思いますが、現実に使われている例は稀でしょう。労力と紙の面積を膨大に必要とするからです。動かないから、面白くないし。
となると、マンガですね。マンガには独自な語彙・文法があるわけですが、コマ運びや表現手法のクセが強くて難読だとしたらどうでしょう？ コマを追えず、ひとつのコマでさえ意味不明となるでしょう。形式的証明記述の現状は、このようなものだと思います。
それで結局、落ち着くところは紙芝居や小説で表現することです。我々が教科書や論文でいつも見ている自然言語で書かれた非形式的証明記述です。絵は補助で「語り」、あるいは「語りだけ」でストーリーを読者に伝える方法です。
「語り」は「絵」に劣ります -- こう言うと奇妙に感じるかも知れませんが、Globularの“絵”に限らず、伝統的な、自然演繹の証明図にしろシーケント計算の証明図にしろ、それは形式化された絵であり、“語り＝自然言語”に比べればずっと精密です。
証明において、形式化された絵（静止画）と、それらを編成・構造化したアニメーションを扱える環境がないことが、さほど難しくもないことまで、無闇と難しいモノにしてしまっている要因でしょう。…… という状況を解決できなくても、状況を知るだけでも「無意味な難しさ」に気付くことはあります。
*1:「台紙に貼ったパラパラ漫画」は、目線のほうを移動しながら、動いているところを想像する方式です。マンガのような語彙・文法（約束ごと）はなくて、単純に静止画を次々と追いかけるだけです。
