Title: Formalising the correct termination, fairness, and tractability of Meek’s method of STV in Isabelle/HOL
Speaker: Jake Palmer
Abstract:

I will present my work on formalising various properties of Meek’s method of STV. So far I have represented and proved the quantities, assumptions, and theorems in the paper “Algorithm 123: Single transferable vote by Meek’s method”, wherein they provide a proof that when some number of candidates are elected at some stage of the process, they remain elected and their votes converge on the quota (i.e. what a candidate needs to be elected) and this converged-to state is unique. I will briefly present some ideas on a more complete proof of correct termination which takes into account filling seats, and some ideas on how to go beyond that to making the notions of fairness and “wasted votes” in Meek rigorous and formally proving they are satisfied by the method. Finally, I will finish off the work by proving the tractability of the method in terms of its time complexity, and extract the verified algorithm.