13 karma · joined June 27, 2019
The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.
As jsantos511 said many times, we need more shots on goal!
Here, a random person in the room announced their birthday, and the question is whether someone else in the room shares that birthday. It's a very different situation, where I'm guessing you need around a thousand people for it to be very likely that their birthdays coincide, compared to the twenty or so for the birthday paradox.
Giant is a good value brand. They make a lot of components in house, so you get cheaper, "good enough" handlebars etc.
In that brand, I'd recommend a used trance 29 or a new trance x 29, depending on your budget. I'm happy to talk about bikes for days!
Trek, Norco, Rocky mountain are also good value. Just about any modern trail bike is excellent.
We considered doing that, but like you also point out, if you had to sign each piece of the torrent, it would slow throughput to a crawl.
The 80% of the time it returns positive, you tell the epidemiologist, and they prevent a few further infections by investigating close personal contacts.