第11夜:証明はむずかしい

数の悪魔*1を題材にして、Schemeの勉強の11回目です。
111...のように1が並んだ数の2乗は、123..321というように対称性があって美しい数字になるというのが、第1夜の数の悪魔の主張でした。ですが、11個並べたら、その数がおかしくなりました。

突然、答えがサラダみたいに、ぐじゃぐじゃの数字になった。そうだったな。あのトリック、なかなかいいと思っていたが、結局、証明なしじゃ、どうにもならんのだ - 数の悪魔

(define (one n)
	(define (display-expr m) (format "~11D x ~11D = ~D~%" m m (* m m)))
	(define (one-iter m n l)
		(if (< n 1)
			(reverse l)
			(one-iter (+ (* m 10) 1) (- n 1) (cons (display-expr m) l))))

	(one-iter 1 n '())
)

(define (main args)
	(print (one 10))
0)

結果はこちら。

(          1 x           1 = 1
          11 x          11 = 121
         111 x         111 = 12321
        1111 x        1111 = 1234321
       11111 x       11111 = 123454321
      111111 x      111111 = 12345654321
     1111111 x     1111111 = 1234567654321
    11111111 x    11111111 = 123456787654321
   111111111 x   111111111 = 12345678987654321
  1111111111 x  1111111111 = 1234567900987654321
)

1が10個並んだところで桁上げが起きて、対称性がなくなっています。本では、証明の重要さと難しさについて、川を渡るときに踏む、石にたとえています。
本来ならば、プログラムも正しさを証明しないといけないと思うのですが……、やはり、とても難しいです。

*1:Hans Magnus Enzensberger,1997,Der Zahlenteufel,エンツェンスベルガー 丘沢静也(訳),2000,数の悪魔,晶文社