stabbles

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.

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.

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

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.

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.

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

Whether you agree with the policy or not, the way it's written is good. It just states the rules neutrally. See https://gcc.gnu.org/ai-policy.html.

In various projects I see AI policies that state not only the rules, but also their (moral) justification. I think that's worse, because I can agree to the rules, but that does not mean I subscribe to your point of view.

Imagine this: OpenAI runs their benchmarks of unreleased models on systems physically disconnected from the internet.