fun Chess Monte Carlo Simulation Tracking the 2026 Candidates with dynamic player strength, one million simulated tournaments per round. Formalization of Tao's Analysis I in Lean 4 A from-the-axioms-up Lean 4 formalization of Terence Tao's Analysis I, covering both the main text and the exercises with no outside libraries. Formalization of “Squares in Circles” in Lean 4 Lean 4 proofs of the smallest circle that holds n unit squares, and of every packing that achieves it, for n = 1 to 8. Optimality and uniqueness of Gerver's sofa in Lean 4 Lean 4 proofs that Gerver's sofa is the largest shape that can be carried around the corner of a hallway, and that it is the only one, up to rigid motions. formalize-math-paper, an agent skill for formalizing papers in Lean 4 An Agent Skill that guides an AI coding agent through formalizing a mathematics paper in Lean 4, from reading the paper to an audited project ready for the Palomar registry. Optimality and uniqueness of Romik's ambidextrous sofa in Lean 4 A Lean 4 proof that Romik's ambidextrous sofa is the largest shape that can turn both right and left around the corner of a hallway, and that it is the only one, up to rigid motions. If Only They Voted Who would have won U.S. elections from 2012 to 2024 if only some voters were counted, for president, Senate, House and governor. The Reinhardt conjecture in Lean 4 A Lean 4 proof that Reinhardt's smoothed octagon packs the plane worst among centrally symmetric convex shapes, and that it is the only worst shape, up to affine maps. work Synthetic Network Generators A pipeline-unified gallery of community-aware synthetic network generators, each illustrated stage by stage on the same small example.
