Title: Formalising the correct convergence of Meek’s method of STV in Isabelle/HOL
Speaker: Jake Palmer
Abstract: I will present an overview of my work so far on formalising a representation of the surplus transfer phase of Meek’s method of STV. I have represented the assumptions characterising the way in which the quota, excess, and votes update given a single update to a candidate’s weight, where the weights represent the current state. I will present some convergence and ordering theorems on weights as well as the theorem in Isabelle characterising the first part of Theorem 1 in the paper “Algorithm 123: Single transferable vote by Meek’s method”. I will briefly present some ideas on the work which will make up the rest of the PhD such as implementing Meek’s method in Isabelle, situating the method within the framework of social choice theory, showing that the method is not susceptible to the butterfly effect in voting, and producing Meek’s method automatically as the output of generating a method/policy for minimising wasted votes in the context of STV.