用 Lean 形式化验证阿拉斯加排序选择选举计票规则

研究以阿拉斯加排序选择选举为案例，用 Lean 形式化该州计票规则的解释并验证其实现，证明选举特定结果。自 2022 年以来阿拉斯加 115 场排序选择选举中，10 场选举的 75 条选票记录被复现公布结果的程序以不同于该解释的方式计数，但未改变任何胜选结果；差异源于超额投票和重复排名，研究还考察了其法律依据。