Nerd Sniping - the Infinite Grid of Resistors This is a formalization in Lean of xkcd's "nerd sniping" question