stabbles

The `-j` is meant for the top-level invocation only, and the $(MAKE) pattern is standard.

The `+` or $(MAKE) "tricks" to ensure the jobserver is inherited in submake and any other subprocess are no longer needed in gmake 4.4 (from 2022) because it defaults to a FIFO instead of pipes. The author should just upgrade gmake :).

What if the tool is more advanced, like an optimizing compiler: `g++ -O3 -march=native -x c++ - <<EOF ... EOF`

If the compiler invocation is sufficiently slow, the llm could consider outputting a binary directly?

For all we know matrix multiplications are a faster way to generate optimized machine code than branchy sequential compiler code with tons of heuristics and passes.

Yeah, "standardizing" change IDs would make it much easier to develop further tooling around it. In particular decentralized review is something that I'd be interested in.

For example, if GitHub is down, that would not be a blocker to access review comments or to do reviews. And maybe you could push your reviews to a GitLab mirror if you want a UI.

An even simpler "sandbox" is to create a separate user and home dir for your LLM.

The reason is that their primary source of truth (traditional database) and their search index (elasticsearch) are out of sync.

The issues/pulls pages used to be showing the data from the primary data source, and then they changed it so everything is search, including the basic props is:pr and state:open.

5 years is great, but I'm sure in Norway they advertise "no flip" / "no turn" / "single-sided" mattresses as a feature too ;)

With sufficient competition, the incentives of companies would change if consumers would be willing to rent instead of owning products. Then planned obsolescence is not to their benefit.

If it is a skill, it's something that can be learned by both humans and LLMs.

Strongly reminiscent of God of the Gaps [1]

[1]: https://en.wikipedia.org/wiki/God_of_the_gaps

Wouldn't AI make the field of mathematics more ambitious? In software development it feels that way: there are often tasks I can take on that would have been too risky in 2025, because it was unclear if they were worth it. Now you generate a prototype and can make much better judgement calls what is possible and what is worth pursuing.

Mathematics is more than establishing arbitrary facts (although some look like curiosities), it's also defining what interesting research directions are and establishing common language/notation. I think that will stay relevant?

The maths community is now in the antithesis phase, synthesis will take a while ;)

Lee Sedol said in an interview that "losing to AI, in a sense, meant my entire world was collapsing. ... I could no longer enjoy the game. So I retired", and I think there will be folks in the mathematical community who would feel the same when the solutions pages to hard problems are suddenly available.

But on the other hand, people learned a lot from chess engines. After decades of chess computers beating humans, there was still a renewed interest in watching Leela beat Stockfish, with many people trying to understand the strategy Leela used.

If your happiness comes from grinding on a problem and making progress, the prospect of having to dig through a corpus of AI-generated proofs might be hard to swallow. But if you're willing to do that, you will still find beautiful things that only so many people can truly appreciate.

Great read, thanks for sharing

It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it).

To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?

Would be nice if they included a few "notable" games in the release notes.

Presumably it's easy to highlight ones from benchmarks where the evaluation of Stockfish 19 is most significantly different from version 18?

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.

341k lines of lean without comments

Similar to https://news.ycombinator.com/item?id=47566442

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

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.

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

Maybe some patterns already surface with 2-grams

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.

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

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 <verb>s no <noun>" instead of "It doesn't <verb> <noun>".

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

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

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

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.

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.

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.