ふと思いついてしまったので，数学の証明をどれだけプログラムっぽく書けるか挑戦してみました．
これがその産物です．
２の平方根が無理数だということの証明を書いてみたのですが，どうですかプログラムっぽいですか？
以前にもやったことがあるのですが，そのときよりうまくできた気がします．やはり背景を暗くするのはプログラムっぽさを増しますね．
数学科の方は，ここで定義されている ord という関数がこういう性質を満たすことが注意されていないじゃないか！と思われるかもしれませんがまあ許してください．確かにそこがいちばん非自明なんですけどね…．
これによって証明が読みやすくなっているかどうかは，ちょっとわかりません．そもそもプログラムも読みにくいものですからね．
もうちょっとたくさんの色でシンタックスハイライトできたら，見やすいかどうかはともかく綺麗だったでしょうね．
皆さんも，もしよかったら挑戦されてみてはいかが．意外と工夫の余地があって楽しいですよ．
