Hacker News: jojomodding

New comment by jojomodding in "Alexander Grothendieck Revolutionized 20th-Century Mathematics"

jojomodding — Sun, 24 May 2026 22:02:42 +0000

Interestingly, the way in which Grothendieck conceived of equality is nowadays being questioned, especially due to the rise of formalized mathematics and Lean. More concretely, there is this fun paper by Kevin Buzzard which deconstructs it: https://arxiv.org/abs/2405.10387

Money quote:

> In this paper I argue that the first assertion above is false, the second is dan- gerous, and the third is meaningless.

New comment by jojomodding in "What Do Gödel's Incompleteness Theorems Mean?"

jojomodding — Thu, 21 May 2026 18:03:35 +0000

This also makes it obvious that at some point, the halting problem becomes "unprovably hard." There must be Turing Machines for which it is independent of the accepted axioms of mathematics whether or not they halt. And indeed, constructing such machines is not too difficult.

There is current research into finding the smallest such Turing Machine. Here is one with 748 states: https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...

New comment by jojomodding in "The Iranian Government Internet Filtering Machine Is Trying to Get Into Mozilla"

jojomodding — Tue, 19 May 2026 18:47:37 +0000

That title is a gross misrepresentation of what is actually happening. This is actually about an Iranian Cloud Provider wanting to be added to the public suffix list.

New comment by jojomodding in "LLM Policy for Rust Compiler"

jojomodding — Fri, 15 May 2026 22:18:50 +0000

Not sure what is particularly autistic about the observation that "couldn't we just all get along" is unfortunately not how the world works even if we would like it to?

New comment by jojomodding in "Bun Rust rewrite: "codebase fails basic miri checks, allows for UB in safe rust""

jojomodding — Fri, 15 May 2026 18:55:46 +0000

exactly. If they wanted to iterate on their port they would add lifetime annotations here, which are the tool Rust be uses to ensure safety. They're just kicking the unsafety block down the road. This accomplishes nothing and is not how you get Rust to deliver its safety promise.

New comment by jojomodding in "Israel's AI targeting system: how data from a phone become a death sentence"

jojomodding — Wed, 13 May 2026 19:36:02 +0000

Or the people that aid and support those people. Systems like this, or the Iranian crackdown on protestors earlier this year, show that in our times, an autocratic regime is able to keep power in spite of significant popular resistance. Revolutions like the fall of communism in 1989/1990 seem impossible now. If you lose democracy once, it's over.

New comment by jojomodding in "Bitter Lessons from the ISSpresso"

jojomodding — Sat, 09 May 2026 19:36:18 +0000

But that's boring. Also it's already happening a lot more than humans are being sent.

New comment by jojomodding in "Grand Theft Oil Futures: Insider traders keep making a killing at our expense"

jojomodding — Thu, 07 May 2026 16:18:05 +0000

Nonvoters implicitly consent to the outcome ahead of time. Which means that they can carry part of the blame--if they didn't like it they could have voted against it.

New comment by jojomodding in "This Month in Ladybird – April 2026"

jojomodding — Sun, 03 May 2026 12:52:19 +0000

Is pdf.js the renderer that VSCode uses? You know, the one where everything becomes extremely blurry when you zoom in for absolutely no reason at all except (I would imagine) developer incompetence?

New comment by jojomodding in "For Linux kernel vulnerabilities, there is no heads-up to distributions"

jojomodding — Thu, 30 Apr 2026 20:07:32 +0000

> are free to sell 0day for profit.

This is not true in many jurisdictions.

New comment by jojomodding in ""People who don't use AI will be left behind""

jojomodding — Wed, 29 Apr 2026 19:47:24 +0000

I sympathise with the author and the argument. I know the text is a rant. As such, I can understand that the proposed consequences might not make sense. Yet still, there is a fun game you can play, where you replace AI by "chess engine" and you get a text that would be fitting for a late 90s chess grandmaster but seen as totally anachronistic today:

"Chess players who don't use engines will be left behind", they say. I can't emphasize enough how much I hate it when I hear/read shit like that because I'm pretty sure, in fact, that what will happen is the exact opposite.

People who rely on engines are the ones who will be left behind. They'll forget how to think, how to move the pieces, how to solve a simple straightforward mate in 3, how to tell victory from stalemate... they'll forget how to fucking LEARN. I think that's the part that makes me the saddest. What a beautiful thing it is just to play chess.

If you think Deep Blue can do better than you, why would you just let it? Why wouldn't you aim to be better, to learn how to be or do something that a chess computer would never do?

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

jojomodding — Mon, 27 Apr 2026 23:11:50 +0000

I do not get why not needing proof objects is desirable. It seems good to have a defined way to store proofs that has a very tight spec and can thus have competing implementations, like in https://arena.lean-lang.org/. The LCF approach couples the proof format to the module system of a programming language.

Occasionally, inspecting that proof term is useful to see what happened in a proof.

Then again, I also like dependent types.

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

jojomodding — Mon, 27 Apr 2026 23:04:44 +0000

Its a software where you type your maths proofs in and a "yes" comes out. Except if your proof is broken, then a "no" comes out. Of course, sometimes the computer is just a bit dumb at intuiting the intermediate steps, so you need to explain like a 10-year-old child (or else you get a "no" as you failed to convince the computer). And storing all these explanations takes memory. And you have to speak the somewhat idiosyncratic language of the computer, which you can imagine a bit like LaTeX but more easily parseable and less ambiguous.

The blog article author is saying that Lean is like a younger child (that needs more intermediate steps explained), stores proofs more inefficiently (taking more memory) and that its computer proof language is harder to read for humans. Additionally there is a technical point about dependent types, which are the principle around which the computer proof language is organized (the same way a programming language might be organized around object-orientism).

New comment by jojomodding in "Microsoft and OpenAI end their exclusive and revenue-sharing deal"

jojomodding — Mon, 27 Apr 2026 19:35:52 +0000

Giving something that has no internal concept of time (or identity for that matter) a prison sentence of n years seems kinda ineffectual.

New comment by jojomodding in "Asahi Linux Progress Linux 7.0"

jojomodding — Sun, 26 Apr 2026 14:27:15 +0000

Nothing is stopping you from using LLMs when contributing to their project (I think). One reason might simply be that they would rather spend the (very sparse) donation money on anything else but tokens.

New comment by jojomodding in "The Free Universal Construction Kit"

jojomodding — Sat, 25 Apr 2026 19:47:07 +0000

Tell your kids about FUCK, the most fun way to play with them bricks...

New comment by jojomodding in "Michael Rabin has died"

jojomodding — Sat, 18 Apr 2026 22:07:15 +0000

actually his uncle.

New comment by jojomodding in "AI-assisted cognition endangers human development?"

jojomodding — Wed, 15 Apr 2026 20:00:25 +0000

And we collectively decided that it's fine, you don't actually need to be able to solve 1234×5678 in your head.

But I am not sure you can compartmentalize the specific skill we can out-source to AI. I would not agree with "you don't need to be able to think in your head."

New comment by jojomodding in "AI Will Be Met with Violence, and Nothing Good Will Come of It"

jojomodding — Sun, 12 Apr 2026 14:42:16 +0000

For a start by not tearing down the systems that kept inequality in check in the past. Like union membership or banking regulation etc. just to name some examples.

New comment by jojomodding in "Rescuing old printers with an in-browser Linux VM bridged to WebUSB over USB/IP"

jojomodding — Tue, 07 Apr 2026 19:08:40 +0000

Is there a Docker-to-WASM pipeline, and how does it do anything differently from emulating x86?