Monsky's Theorem

Source: doi:10.2307/2317329 Authors: Dhyan Aranha, contributors Status: verified Main declarations: LeanPool.Monsky.monsky_theorem Tags: geometry, combinatorics, measure-theory MSC: 52C20, 05B45

Mathematical overview

This project formalizes Monsky's theorem: a square can be dissected into n triangles of equal area if and only if n is nonzero and even. The proof constructs a non-Archimedean valuation on the real numbers, uses it to define Monsky's three-coloring of the unit square, proves that an odd equal-area triangulation would contain a forbidden rainbow triangle, and constructs the standard even dissections.