imo, partially because it's still not easy (in terms of code -> formal proof). With AI, I've been Lean-ifying a simpler (but non-trivial) algo. Pointing (current) AI at it only goes so far and in fact might go "too far" in certain cases, where a non-formalized argument would have sufficed. There's also "who watches the watcher" -- did it really prove what we're supposed to prove?
For something like these compression algos, though, I imagine it would be much easier since they already have actual proofs out there.
"maybe even psychologists" -- unironically true, but maybe I am talking about something different from you. The basis of (higher-level) math seem to mostly be "am I psychologically (emotionally...?) comfortable with accepting annoying ideas?" At least from my experience.
(not the above poster but) I set up a local workspace for it to read/write from, so that edit is effectively just VSCode/vim. Unfortunately, it seems more verbose when writing out to file.
Back of the envelope math, if anyone wants to correct my mental model: 2.1B (mincore)/week ~ 300M (mincore)/day. Assuming ~300k cores (~3k physical server CPUs, seems fine), that's 1k min/day. Seems about right, though obviously not uniformly distributed.
In any case, the number I'm focusing on here is the 300k cores part (x2 if you're counting in vcores). It does not seem like too much to ask for (significantly) more than that at github scale. It doesn't feel like a hardware issue, is what I'm getting at.
I decided to ask chatgpt for a fermi estimate of cores/datacenter, which you can check for yourself: 1~10 million physical cores. The surprising part of this for me was the "low" power usage (it used 20MW/"datacenter" as another point for estimation).
1MW ~ 6700 NYC citizens' residential usage, apparently, lol. I don't know exactly why, but that citizen number seemed a surprisingly large (well, probably because I've played with approximately-MW lasers).
I don't GR but I'm fairly certain dipole does not work for gravitational waves (i.e. two objects accelerating straight at each other). Supposedly, there's a specific definition of "gravitational wave" here. You can, of course, detect the change in gravity though, regardless of "gravitational wave" or not.
... I don't think the original commenter said anything about mice being a non-model organism.
But mice are far from humans, and I, at least, find the distinction rather important.
For something like these compression algos, though, I imagine it would be much easier since they already have actual proofs out there.
reply