Hacker News: zodiac

New comment by zodiac in "“Why not just use Lean?”"

zodiac — Mon, 27 Apr 2026 22:52:04 +0000

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.

New comment by zodiac in "Some Junk Theorems in Lean"

zodiac — Sat, 27 Dec 2025 15:46:21 +0000

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

New comment by zodiac in "Ladybird passes the Apple 90% threshold on web-platform-tests"

zodiac — Mon, 06 Oct 2025 19:17:01 +0000

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

New comment by zodiac in "Trump to impose $100k fee for H-1B worker visas, White House says"

zodiac — Fri, 19 Sep 2025 22:59:58 +0000

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

New comment by zodiac in "Planes in 3D Space"

zodiac — Sat, 27 Apr 2024 17:26:21 +0000

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

New comment by zodiac in "EU Probes Apple's Decision to Shut Down Epic's Developer Account"

zodiac — Fri, 08 Mar 2024 13:17:00 +0000

> 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".

New comment by zodiac in "The "missing" graph datatype already exists. It was invented in the '70s"

zodiac — Wed, 06 Mar 2024 00:58:06 +0000

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?

New comment by zodiac in "Python datetime pitfalls, and what libraries are (not) doing about it"

zodiac — Sun, 18 Feb 2024 15:33:32 +0000

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

New comment by zodiac in "AlphaGeometry: An Olympiad-level AI system for geometry"

zodiac — Wed, 17 Jan 2024 18:52:32 +0000

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.

New comment by zodiac in "A copy-and-patch JIT compiler for CPython"

zodiac — Tue, 26 Dec 2023 16:58:04 +0000

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

New comment by zodiac in "Ask yourself dumb questions and answer them (2020)"

zodiac — Mon, 25 Dec 2023 10:10:23 +0000

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.

New comment by zodiac in "Superrational"

zodiac — Sun, 09 Jul 2023 18:00:20 +0000

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

New comment by zodiac in "The Art of LaTeX: Common mistakes and advice for typesetting proofs"

zodiac — Sun, 08 Jan 2023 18:26:27 +0000

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

New comment by zodiac in "Maids trafficked and sold to wealthy Saudis on black market"

zodiac — Thu, 29 Dec 2022 17:27:28 +0000

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

New comment by zodiac in "Algorithms for competitive programming"

zodiac — Tue, 20 Sep 2022 06:37:46 +0000

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.

New comment by zodiac in "Timing of daily calorie loading affects appetite and hunger responses"

zodiac — Fri, 16 Sep 2022 13:04:33 +0000

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”?

New comment by zodiac in "Timing of daily calorie loading affects appetite and hunger responses"

zodiac — Fri, 16 Sep 2022 12:57:19 +0000

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

New comment by zodiac in "Edge Case Poisoning (2020)"

zodiac — Fri, 09 Sep 2022 07:48:25 +0000

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.

New comment by zodiac in "Mainnet Merge Announcement"

zodiac — Thu, 25 Aug 2022 15:25:53 +0000

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".

New comment by zodiac in "Mainnet Merge Announcement"

zodiac — Thu, 25 Aug 2022 03:00:47 +0000

> 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).