上回談到了 在學習 Lean 4 語言寫數學證明
開發者蓋的遊戲網頁非常好玩，我也很想把每個主題都玩完
但總覺得該是時候來碰一些比較實際的專案了
遊戲是某種精心設計，讓難度慢慢加強，吸引玩家黏著卻不放棄。實際的專案可以得到現實迎面一記的巴掌，比較能感受真的使用這個語言會碰到什麼樣的挑戰。
我想選一個稍微有點難度，但又不會太難的公式來證看看。要做的事情就是把紙上的公式變成 Lean 4 語言的程式碼。
最後選了「阿羅不可能定理（Arrow’s Impossibility Theorem）」。這是個經濟學教科書都會提到的定理。不少科普頻道也介紹過這個題目。
我找了一篇 2012 的論文（ Yu 2012 ），內容短短的，證明就一頁的篇幅。非常的 self contained
不可能出什麼問題對吧
關於阿羅不可能定理
Kenneth Arrow 證明：不可能設計出一種理想的投票機制，能夠理性的反映出選民的偏好。
投票機制可以看成一種機器：輸入是人們的對各種選項的偏好順序，寫在選票上。輸出是某種社會偏好，好像社會是一個人一樣，也對各種選項有偏好順序。
票箱把選票吃進去之後，人們把票箱打開，用某種演算法瞎忙一陣（例如計算得票最多的候選人），得到社會的共識：例如選民最喜歡哪個候選人。
假設你的選票不只能寫最喜歡誰，還能寫第二喜歡的人，一路寫到最不喜歡的人。選票也能允許你對有些選項一樣喜歡。那你有辦法設計一個演算法，從每個人選票的資訊，得到一個不錯的社會偏好嗎？
首先我們得討論「不錯」的定義是什麼。
阿羅先訂出了這個投票機制一些很基本的三個要求：
首先機制應該尊重選民「一致（ Unanimity）」的偏好 ：如果所有選民偏好 A 選項優於 B 選項，那投票機制產生的社會偏好也要是 A 選項優於 B 選項。
再來，「無關選項無干結果（Independence of Irrelevant Alternatives）」：如果票箱開出來的結果是偏好 A 優於 B 。現在再把選票全部倒出來，保留所有的 A 和 B ，但把每張選票的 C 選項位置任意調整。。C 是和 A B無關的選項，開票結果對於 A 與 B 的順序不該改變。
最後，「不能獨裁」。不能有個選民比較「特別」，他的偏好是什麼，票開出來的結果就是什麼。
非常遺憾，阿羅證明，三個非常無辜、基本的要求不可兼得。
證明的大方向就是：假設有個投票機制符合「尊重一致的偏好」與「無關選項無干結果」，這會導向一個結論：這個機制存在一個獨裁者可以左右開票結果。
實作過程
在開始實作前，我先讓 Claude 看了一下論文。和他說給我一點指引，但不要幫我寫任何程式。這個專案的目的是練習語言。
第一天的前幾個小時，我在 AI 指示之下完成了「尊重一致的偏好」、「無關選項無干結果」、「不能獨裁」的三個定義。
我感到超有信心，想不到可能一天就能完成專案了。
然而 …
寫這篇文的時候，是已經經過了痛苦的兩個星期。無數想放棄的念頭，和 AI 求饒請他直接把程式都寫完。我心裡那隻泅泳的老鼠已經要沈到水底了。
我可以感受到中學老師分享那種中學生在 AI 面前鬼打牆「你再講簡單一點 …」 的那種無助感。
和 AI 求饒也沒用。在問題小的地方時，例如一個定義好的引理（ Lemma），AI 可以暴力產出一堆很醜的程式碼，但完成證明。在問題變大變複雜時，AI 還是可以暴力產出一堆很醜的程式碼，但什麼都沒證出來。
在 Lean 裡面，你可以把該某個引理的命題先寫出來，然後證明的部分先留下一個 sorry 。編譯器看到 sorry 之後會壓下所有的錯誤訊息，但留下黃字警告，代表有些證明還沒完成。
AI 常常會瞎忙一陣，然後在程式碼中留下一堆 sorry ，再把爛攤子推回來給我。
他的白話回覆則沒那麼充滿歉意。我能辨認出他開始亂繞的句子： ”But actually the cleanest approach …“ 當這句話出現的時候，要解的問題大概超出他的能力範圍了
這裡再講一下我用了什麼 AI 。主要這三種： Sonnet 4.6 ：一般腦漿，萬事不決、疑難雜症、語法問題、蠢問題問 Sonnet 。 Opus 4.6 ：高級腦漿，魔力消耗比較多。複雜問題、Sonnet 處理不來的問題問 Opus
Claude Code ：真的想讓 AI 完成實作，或除錯用這個。他能真的變動程式碼，跑編譯並看錯誤訊息。他也有比較長的腦內小劇場。
困難之處
困難點可能來自幾個地方：題目的部分和語言的部分。
第一是阿羅不可能定理，幾乎看不到嚴謹的證明。幾乎所有論文、 YouTube 影片的介紹或「證明」都是用某種例子和英文口語描述。很少有充滿數學符號的描述。
這可以理解，畢竟要知道這個定理的原因是不要再妄想設計一個完美投票機制。或是真的要妄想設計一個完美投票機制，要知道有坐大山擋在這，不要走一些冤枉路。
那些數學細節可能阻礙高層次的理解和建立直覺，但對要用程式重製證明，則會很有幫助。
語言的部分，在初期的過程，我很難搞清楚哪些是「電腦」的部分，哪些是「數學」的部分。
論文寫 “Consider any preference profile… such that … ” ，我不能只「考慮一下」，必須建構出來。但這個建構出來，我是要用電腦的方式建立一個例子，還是應該用數學的方式建立一個集合，裡面有所有的元素？
兩種都很痛苦的嘗試過了。 學到了什麼 Decidablility 、noncomputable、選擇原理– 你如果要把某個命題放到 if else 條件式裡面判斷真偽，你必須假設有某種有效率的演算法可以判斷真偽。都是一些我現在還不太敢看的兔子坑。
在電腦裡面，要處理加一減一這種差一號的數數問題，有很多可以變通的方式。要在數學證明處理，就變成超級麻煩。要不就是得假設某個自然數不等於零，然後另外證明其大於零。要不就是要對各種「是不是零」的狀況做討論。
證明細節
各種論文會說證明阿羅不可能定理有兩種主流方式，但另一種我幾乎沒看課本或影片介紹過了。所以可能就算一種主流方式。
2012 這篇論文是主流方式的濃縮精簡版。
阿羅不可能定理有個假設是要有三個或以上的選項。
假設我們把選民編號。票箱內所有選票全部都偏好 A 優於 B ，然後選民一個接著一個，把偏好改成喜歡 B 多於 A 。
「尊重一致偏好」這個原則說：在這個過程的開始，社會共識會是 A 優於 B 。而過程結束時是 B 優於 A 。因為在過程中的這兩個點，選民有一致意見。
而在這個過程中，一定是在中間哪裡，社會對 A B 的共識翻了過來。肯定會有一個關鍵選民 阿財，阿財在改選票前，社會共識還是 A 優於 B ；阿財改完選票之後社會共識變成 B 優於 A 。
論文再拿出兩捆新的神奇選票。卡一個無關選項 C 在中間。根據一頓神奇的操作，論文列了一個唯一字體置中的引理，旁邊標了無敵星星（*）： 原來 A B 兩個選項的關鍵選民阿財，也能控制 B C 兩個選項的投票結果。
這個無敵星星引理再一頓操作之後。阿財一路提權，變成任何兩個任意選項 X Y，阿財喜歡 X 優於 Y ，投票結果就是 X 優於 Y 。
我們發現喊水會結凍的阿財，其實是獨裁的阿裁。
最後的卡關
我在前進到論文最後剩下兩句話的時候嚴重卡關。
第一句話是某個和 B C 有關的結果可以「很容易（easily）」推廣到任意選項 X Y 。那個很容易的部分我一直沒參透，高級腦漿 Opus 也沒理出個頭緒。
最後我完成的結果是要分 13 組情況做討論，大概 80 行程式碼。不知道有沒有符合 easily 的定義。
Lean 4 有很酷的「不失一般性」 wlog 指令可以用。想要證明 x y : ℕ 且 x ≠ y ，則 min x y ≠ max x y 。如果沒特別處理，需要對 x 和 y 用同樣的方式各證明一遍。但不失一般性可以把 x y 參數對調，重新套入第一遍證好的結論，就不用證兩遍。
不過我慧根不夠，沒看出那 13 組情況哪裡有「一般性」可以用。
AI 救援成功
但我有問高級腦漿一題，他有神助攻。我問說我們現在證明卡關，有沒有我前面做錯了什麼？或是我現在做些甚麼誰能讓我們的日子好過一點（Make our lives easier）嗎？
他說我的關鍵選民的座號，都是用某個「存在性」證明得到的。因此這個變數和其條件（關鍵選民影響社會共識）都沒辦法被其他引理分享。我應該把關鍵選民的座號，用 Mathlib 套件的 Fin.Find API 改成「定義式」的，這樣所有引理都可以拿到同樣一個變數。
這個變化花了一天執行下去後，效果十分顯著。原本後面關鍵的無敵星星引理，引用時要給一堆雜七雜八變數和條件。
把關鍵選民改成定義式之後，所有重要引理只需要這幾樣假設：三個選項 A B C ，三個選項相異 A ≠ B ≠ C ，「尊重一致偏好」，「無關選項無干結果」。
這一改下去之後，後面完成證明的路就暢通了。而且也能清楚看出，證明的過程就是玩弄三個相異的選項，在不同排列組合之下，為了符合「尊重一致偏好」和「無關選項無干結果」兩個條件，我們成功把阿財拱成獨裁者。
疏漏之處
編譯器會檢查所有證明的過程有沒有正確。
完成證明的引理或定理，在 VSCode 編輯器邊邊會搭上藍色勾勾。
證明完成是完成了，上傳 GitHub 上，自動化測試會再打上綠色勾勾
可是就像另外一篇形式驗證論文所提到：我這麼瞎忙一陣，證出來的東西是阿羅不可能定理嗎？
我怎麼知道我描述要證的題目，和論文裡的題目是一樣的？
極端而言，我也可以證明 1+1=2 ，然後宣稱這是阿羅定理，而且所有機器方面能給的勾勾都拿到了
也許我哪個條件訂得太寬？證明出來的只是一個長得像阿羅定理但實際上不是？
某方面確實是有個技術債還沒還。我用的數學順序結構並非經濟學上的偏好。因此論文中的弱偏好並沒有在程式中反映出來。
但還好我有欠這個技術債。要是之前在那邊講究這個弱偏好，估計根本整個專案沒法完成。
這裡也覺得證明變成程式碼之後有個好處。就是可以看到性質的依賴是怎麼發生的。例如我的順序結構中多了不該有的「反對稱關係」，把它移除掉之後可以看到錯誤會傳染到哪裡，後面哪些結論會壞掉。
結論
到底我從這個關於投票最重要的數學結論之一，得到什麼對民主的體悟嗎？
完全沒有 ！！！！
我只覺得形式驗證就是一種苦力活。能叫 AI 做就叫 AI 做。人不要受這種罪
完成品 https://github.com/ChihChengLiang/arrow
歡迎交流指正
如果你有用不完的 AI 額度，也歡迎告訴我大概 AI 從無到有完成這個專案需要多久