zodiac

It appears that Anthropic has released a proof as well (same bounds), but with a different approach? https://drive.google.com/drive/u/0/folders/1uaWnPqWkXy1sjfsD...

Does this require having a Rocq semantics of LLVM IR? Which one do you use?

In this case (the PHP bug), the "AI cycle" may have exposed the security vulnerability but it did not create it. If someone released a non-AI-based static analysis tool that was really good at exposing vulnerabilities I wouldn't expect that person to foot the bill of fixing the exposed vulnerabilities

Tokens are not the bottleneck for filling in these gaps in mathlib. Human review and growing the specialized expertise needed for human review are. https://leanprover-community.github.io/contribute/index.html...

Does snapshot/suspend/resume keep processes/RAM alive - or do you need to re-start processes/reload stuff into RAM? How does that work under the hood (CRIU?) and how fast is it?

We still care about computation and algorithms even when proving theorems in a classical setting!

For e.g., imagine I'm trying to prove the theorem "x divides 6 => x != 5". Of course, one way would be to develop some general lemma about non-divisibility, but a different hacky way might be to say "if x divides 6 then x ∈ {1, 2, 3, 6}, split into 4 cases, check that x != 5 holds in all cases". That first step requires an algorithm to go from a given number to its list of divisors, not just an existence proof that such a finite list exists.

Here’s a good document defending the merits of this design. https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

No browser passes 100% of WPT, the leader is chrome which has about 1000 failing tests

1400 x $100,000 is $140 million, not $1.4 billion

Interesting, in this representation a plane is represented by the point on it closest to the origin, right?

> Every time you install an open-source app, the developers are extorted by Apple with Core Technology Fee of €0.5 each

I don't think this is true? AIUI a developer can choose to operating using the "old business terms" even in the EU, in which case they don't have to pay the fee. https://developer.apple.com/support/core-technology-fee/ backs this up by stating that the CTF is an element of the "new business terms".

I'm curious about graph algorithms that are "higher order" than what the article describes - e.g. how does Datalog encode the fact that two graphs (given as two relation sets) are isomorphic? How do I write a graph isomorphism algorithm in Datalog, or e.g. enumerate all graphs that have 6 vertices?

Something like "schedule a reminder to stop using the computer at 10pm so I can sleep by 11pm"? Since I want to sleep at 11pm local time every day

The real TIL (to me) is that the previous state-of-the-art could solve 10 of these! I'd heard there was a decision algorithm for plane geometry problems but I didn't know it was a practical one. Some searching turned up http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf as a reference.

I think there’s syntactic ambiguity whether “faster” modifies “generates” or “code”

I read mathematics on screens but when it comes to working out exercises etc I still prefer to do it with pen and paper, so I prefer succinct notation.

I didn’t really get that joke, could you explain it?

The “except for math” part is doing a lot I think. There’s a huge amount of work needed to get rendered math to look as good as latex’s and I’m not sure CSS (as an example) is expressive enough to get this done

“Give us your passport or we’ll fire you / won’t give you this job”

I wish discussions of such site didn't inevitably become discussions about software engineer interviews. It's a really nice site created by volunteers and I've often had it been the only decent resource online for a particular topic, if you want to use it as a reference their "terse but accurate" style for the prose and the compact working C++ code is really nice. And it covers some topics (e.g. treaps) which I've never seen appear in software engineer interviews.

Could you please define “strategy” such that those people you refer to aren’t “following a strategy” but someone who doesn’t eat breakfast is “following a strategy”?

I eat breakfast when I’m strength training and don’t when I’m not, I’m not obese (16% body fat by dexa scan), so is skipping breakfast a “strategy”?

What makes skipping meals a “strategy” while your meal eating habits is (presumably) not a “strategy”?

The article gives one example - find out if a recipe has ingredient X. You could also imagine "find all recipes (from a cookbook) that are vegan", or "find all recipes I could follow given the contents of my fridge", etc.

I agree with your 3rd, 4th, and 5th sentences, but not with your 1st and 2nd. Assuming a large number of independent validators, the Nash equilibrium is close to "there is no equivocation, hence no slashable evidence, hence no incentive to run a slasher node". (Remember that Nash equilibrium implicitly assumes that agents are not allowed to cooperate with each other). Suppose some fraction of the validators are deviating from this equilibrium by doing lots of equivocation, now there is an incentive to run a slasher node. So what this modelling suggests is that in the real world, we can have a small number of slashers and a large number of validators, and the security comes from the fact that anyone could be a slasher (it's OK that the number of people who actually are is small). But we cannot conclude that "it's OK to have a small number of validators, as long as anyone can be a validator".

> Which sure sounds like a decentralized process that is ultimately just centralized around the ETH foundation at the end of the day.

The validators need to be decentralized (i.e. prevent "harmful collusion"), but the slashers don't need to be in the same way (as long as the validators are).

Depends on what you mean by "best". For e.g. comparison-based sorting will already cost O(n log n) time but the HashMap solution will run in O(n) HashMap operations.

The chord is D-flat dominant 7

It’s the same example as on the wiki page for “tritone substitution” - ‘For example, in the key of C major one can use D♭7 instead of G7.’

I think the problem is that the first separates words by underscore and the second doesn’t

Maybe the_svd_doctor uses flop/s to describe hardware, like you said

50ms is under human detection?

maybe 50ms is under the "conscious detection" threshold (debateable, IMO...) but it will definitely feels "laggy"