stabbles

8 ms·

1.
by stabbles 3d ago
Strongly reminiscent of God of the Gaps [1] [1]: https://en.wikipedia.org/wiki/God_of_the_gaps
2.
by stabbles 4d ago
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 gene
3.
by stabbles 5d ago
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?
4.
by stabbles 5d ago
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&
5.
by stabbles 6d ago
Great read, thanks for sharing
6.
by stabbles 6d ago
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
7.
by stabbles 6d ago
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?
8.
by stabbles 8d ago
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.
9.
by stabbles 8d ago
341k lines of lean without comments
10.
by stabbles 8d ago
Similar to https://news.ycombinator.com/item?id=47566442
11.
by stabbles 9d ago
> 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 pop
12.
by stabbles 12d ago
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
13.
by stabbles 12d ago
Now /simplify. Can it be half the size? Will someone at some point prove that the proof cannot be simplified further?
14.
by stabbles 19d ago
Maybe some patterns already surface with 2-grams
15.
by stabbles 19d ago
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
16.
by stabbles 19d ago
That's true, but Claude's use of it resolves no ambiguity.
17.
by stabbles 20d ago
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 <ve
18.
by stabbles 21d ago
I'm sure you've stumbled upon graphs that are not trees, which can be represented with tables.
19.
by stabbles 26d ago
Yeah, Claude insists on prompt-affirming comments, and often refers to the previous draft or implementation instead of the status quo.
20.
by stabbles 26d ago
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/review
21.
by stabbles 1mo ago
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 train
22.
by stabbles 1mo ago
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 - 1
23.
by stabbles 1mo ago
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.
24.
by stabbles 1mo ago
It will just thread some load-bearing seams through the paragraphs.
25.
by stabbles 1mo ago
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.
26.
by stabbles 1mo ago
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.
27.
by stabbles 1mo ago
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 d
28.
by stabbles 2mo ago
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, b
29.
by stabbles 2mo ago
Imagine this: OpenAI runs their benchmarks of unreleased models on systems physically disconnected from the internet.
30.
by stabbles 2mo ago
To be fair, many shells have command caching, so they effectively roll their own exec syscall wrapper: $ python3 -c 'print("hi")' hi $ hash hits command 1 /usr/bin/python3

More ›