arithmetic-kakeya

Lean 4 proofs of two finite bridges for the Epoch FrontierMath arithmetic Kakeya problem: rational forcing equals integer forcing, and every completed configuration leaves two independent surviving labels on each nonempty cut. Companion to the Certified Obstructions paper.

Certified obstructions and exact forcing for the Earth-Moon and arithmetic Kakeya problems — paper, checkable certificates, full replay.