The octahedron recurrence is a recurrence defined on a three dimensional lattice; it was first introduced to cominatorialists by Propp. If we fix a roughly two-dimensional set of initial conditions, all of the other values of the reucrrence are rational expressions in the initial terms. Propp conjectured and Fomin and Zelevinsky proved that in each recurrence these rational expressions are actually Laurent polynomials. Propp additionally conjectured that the coefficients of these Laurent polynomials were all 1. I will describe a combinatorial proof of Propp's conjecture, which shows that these coefficients describe perfect matchings of a family of graphs, and give a way to sample random matchings from these graphs. Depending on time, I hope to talk about ongoing work with Dylan Thurston and Andre Henriques, attempting to generalize these results to higher dimensional lattices.