On: Bloom filters debunked: Dispelling 30 Years of bad math with Coq

This is interesting stuff! It's especially nice to see some more details behind the math -- I did some stuff with bloom filters for work and found that the math didn't always seem to line up with what we'd expect during tests. I wonder if it needs some adjustment...