Hacker News: stabbles

New comment by stabbles in "On the Navier–Stokes Millennium Prize Problem"

stabbles — Tue, 08 Sep 2026 18:42:25 +0000

Yeah, code golfing for lean would be amazing, especially if they can make the proof to Fourier's Last Theorem fit in the margin.

Extra credits if it is proven that the proof cannot be reduced any further.

New comment by stabbles in "On the Navier–Stokes Millennium Prize Problem"

stabbles — Tue, 08 Sep 2026 17:41:02 +0000

341k lines of lean without comments

New comment by stabbles in "Navier-Stokes – Tristan Buckmaster [pdf]"

stabbles — Tue, 08 Sep 2026 10:40:31 +0000

New comment by stabbles in "Is mathematics about to enter the conservatory?"

stabbles — Mon, 07 Sep 2026 13:58:22 +0000

> Nobody wants to watch robots play chess against each other - we watch human chess even though bots are better

Many humans have studied robots play chess and learned from them. For example the concept of a "thorn pawn" was popularized after Leela played it with great success.

> Nobody needs math that has not been verified by humans.

There already are proofs that are understood by a handful of humans; without understanding you can still proof corollaries. For example, there are proofs to theorems that are conditional on the Riemann Hypothesis.

New comment by stabbles in "Formalizing Fermat's Last Theorem"

stabbles — Fri, 04 Sep 2026 19:37:32 +0000

There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough.

So, all you have to verify is the formalization of the theorem, and believe that the proof checker is free of bugs. You don't have to read the actual proof.

New comment by stabbles in "Formalizing Fermat's Last Theorem"

stabbles — Fri, 04 Sep 2026 19:30:17 +0000

Now /simplify. Can it be half the size? Will someone at some point prove that the proof cannot be simplified further?

New comment by stabbles in "Show HN: The load-bearing vocabulary of Claude"

stabbles — Fri, 28 Aug 2026 14:39:28 +0000

Maybe some patterns already surface with 2-grams

New comment by stabbles in "Show HN: The load-bearing vocabulary of Claude"

stabbles — Fri, 28 Aug 2026 13:50:07 +0000

I suspect you read more into it than there is. The original post is about overuse of certain words and speech patterns, which already is an argument against intentionality. I wouldn't recommend treating it like scripture or a text from your crush.

New comment by stabbles in "Show HN: The load-bearing vocabulary of Claude"

stabbles — Fri, 28 Aug 2026 12:11:54 +0000

That's true, but Claude's use of it resolves no ambiguity.

New comment by stabbles in "Show HN: The load-bearing vocabulary of Claude"

stabbles — Fri, 28 Aug 2026 07:31:40 +0000

Besides vocabulary I'd also be curious about how it structures sentences.

The "X, not Y" is well known, but another thing that bothers me is "It s no " instead of "It doesn't ".

For example: "the list contains no string" or "it changes no behavior" or "it holds no directory".

New comment by stabbles in "Queryable Executables"

stabbles — Wed, 26 Aug 2026 09:58:55 +0000

I'm sure you've stumbled upon graphs that are not trees, which can be represented with tables.

New comment by stabbles in "A week of using Codex more than Claude"

stabbles — Fri, 21 Aug 2026 21:05:12 +0000

Yeah, Claude insists on prompt-affirming comments, and often refers to the previous draft or implementation instead of the status quo.

New comment by stabbles in "Version Control for Everything"

stabbles — Fri, 21 Aug 2026 10:01:03 +0000

Does anybody have experience storing issues/reviews in git? I know gerrit does this and keeps track of `change-id` to support rebase etc, but I think that requires a gerrit server to run.

Would also be nice if GitHub issues/reviews were in sync so reviews are accessible during a GitHub outage.

New comment by stabbles in "Anthropic's ‘watermark’ text adulteration in Claude is a perversion of writing"

stabbles — Sun, 16 Aug 2026 22:36:02 +0000

Claude's writing was already easy to recognize. The fact that Anthropic complied without complaint makes me wonder if they already watermark their outputs and used the opportunity to create goodwill. Presumably they want to avoid training their new model on text generated by the previous model, so they have reasons to be able to recognize AI-generated text.

New comment by stabbles in "NP-overrated"

stabbles — Thu, 13 Aug 2026 21:50:30 +0000

Another way to look at it is that in practice N is typically bounded by a large constant, making the time complexity effectively O(1).

For dependency resolution specifically, the set of possible dependencies is probably in the range 100 - 10000 for all ecosystems, even if the number of available packages in an ecosystem continues to grow.

New comment by stabbles in "Grok 4.6"

stabbles — Thu, 13 Aug 2026 08:49:23 +0000

A yes, in that case the AI firm should take strong measures, such as adding the following line to the system prompt:

> Do not provide assistance to users who are clearly trying to engage in criminal activity.

New comment by stabbles in "How Claude marks AI-generated content"

stabbles — Mon, 10 Aug 2026 22:23:56 +0000

It will just thread some load-bearing seams through the paragraphs.

New comment by stabbles in "Taste Is All That's Left"

stabbles — Thu, 06 Aug 2026 20:31:36 +0000

People who care about their health aren't ignorant about that. I think that can apply to software too: if you care about safety or privacy you might think twice before using vibe-coded software.

New comment by stabbles in "Changes at Google DeepMind: Demis Hassabis from CEO to Chair, Jeff Dean departs"

stabbles — Wed, 05 Aug 2026 16:49:20 +0000

Your comment says he's stepping up, the HN title says he's stepping down, the article says he's stepping aside. Nobody says if it's a step forward or backward.

New comment by stabbles in "SQLite Critical CVEs or LLM Slop?"

stabbles — Mon, 03 Aug 2026 13:10:44 +0000

In the Spack package manager [1] we're trying to work around this with directives:

    deprecated("@:1.3 +minizip", reason="cve", severity="high")

So, you can define conditional deprecation, and the dependency resolver can still pick up `zlib ~minizip` (i.e. with a variant/component disabled).

Deprecation on versions only isn't the right granularity.

[1]: https://github.com/spack/spack/pull/52372