Hindman's Theorem: An Ultrafilter Argument in Second Order Arithmetic - Henry Towsner (2009)