兩篇

一番交涉之後，我打算在隨機客的 group meeting 上報告兩篇 papers：一篇是指定的 STOC/FOCS/SODA paper，一篇是 AoPA。要把 AoPA 報告給 outsiders 可不太容易，因為這可以算是介紹整個（兩個？）領域，昨天甚至為此失眠 XD。AoP 的部份我還比較不擔心，proof-checking 要弄得有吸引力可真不簡單。現在我的如意算盤是 proof-checking 的部份找兩個人幫我背書，先由 Knuth 開頭：

Science is knowledge which we understand so well that we can teach it to a computer; and if we don’t fully understand something, it is an art to deal with it. (Computer programming as an art)

最後由 Pollack 收尾：

Many people who pursue formal mathematics are seeking the beauty of complete concreteness, which contributes to their own appreciation of the material being formalised, while to many outside the field formalisation is “just filling in the details” of conventional mathematics. But “just” might be infeasible unless serious thought is given to representation of both the logic of formalisation and the mathematics being formalised. (How to believe a machine-checked proof)

實質內容再慢慢填嘍。

今日飲食：晚上紅油牛腩拉麵 @ 有勁蘭州拉麵（$140）+ 沙茶麵 @ 家（$0）。合計 $140。

--
希望到時候反應不要太冷淡或敵對 XD。