Stories by mathfan

Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean

Asymptotically optimal approximate Hadamard matrices

Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT

Sebastien Bubeck: Another twist in the Erdős problems story

Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT

We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT

The clustering behavior of sliding windows

Math Exposition on YouTube

You want ugly voting districts [video]

You Want Voting Districts to Be Only 4% Pretty [video]

You Want Voting Districts to Be Only 4% Pretty [video]

Why You Want Voting Districts to Be Only 4% Pretty [video]

Utility Ghost: Gamified redistricting with partisan symmetry

Utility Ghost: Gamified redistricting with partisan symmetry

Redistricting as an NP-Hard Problem

Fair redistricting is NP-hard

Fair redistricting is hard

Gerrymandering with geographically compact districts

Partisan gerrymandering with geographically compact districts

Stop criticizing bizarrely shaped voting districts