Hacker Newsnew | past | comments | ask | show | jobs | submit | kingstnap's commentslogin

As someone who used to use it a ton, Reddit is such a shadow of its former self that it's insane. It's actually like 90% bots. Their user growth numbers are all fake. The only real people on there are marketers making fake posts about an issue and commenting using alts and promoting a solution as a form of "AI engine optimization."

Performance problems in theorem provers is an old topic. I remember watching this and it was fun.

https://youtu.be/m-iGCCuHBvY

[Talk] 10 years of superlinear slowness in Coq (2022)


This is pretty interesting in a lot of non-surface-level ways.

I can see OpenAI pushing for this as a sort of more durable moat compared to the now huge number of agentic harnesses that run on your own machine.

This might be getting the foot into some sort of bundling as well. Like unrestricted models or custom fine tuned agents inside this and not providing direct APIs to those endpoints.

That being said I don't see a lot of reasons for people to jump on this if it doesn't bundle something killer. Like to me the fact that GPT Work runs on your own machines and all the artifacts and work in progress there for you to look at is sort of the whole point. I don't just want a final artifact.


>GPT Work runs on your own machines...is sort of the whole point.

Which is also why they want to remove it from your machine. Call it conspiratorial, but I keep thinking about "You'll own nothing and be happy." It seems like the industry is quickly moving in a direction where devices are turning into gateway into the cloud, and personal computing will turn into a hobby that prices out the average individual.


I mean, they didn't say "you can't download the product of your work" or something.

Sure, but neither did I. I summarized the quote, but OP's full quote included the the value of having the work artifacts and works-in-progress on your system to look at. If you are developing software on a VM, there will still be tools to view the artifacts remotely, but this Agents API is still a sign of local development trending away.

Replace hire with marry and this is *exactly* what politics was globally for all of human history.

This is not something "behind us" btw.


> hey Claude vibeslop me a CUDA Anubis solver" route is on its way to being fundamentally dead.

Lmao yeah no. I don't think a little argon2 is going to change shit all.

I mean the thesis of Anubis itself is "scrappers are compute limited (in ways that consumer devices are not)" which has its own massive flaws.


The goal isn't to eliminate scrapers, its to prevent a distributed scraping network from requesting 10000 pages a second each from 10000 different websites.

Yes, I also strongly suspect that this is only going to move more parts of scrapers onto consumer devices. The egress proxies are already there, why not use a little bit of the compute as well?

When you force a low end device to burn CPU or fill ram constantly, the owner throws it out and buys a new one.

Haha, no. The average tech illiterate person tolerates a LOT when it comes to bad performance on low end devices.

The malware already results in noticeable slowdown just running the scraper. Solving anubis challenges is significantly more difficult than simply requesting the page, so it is not feasible on-device without making the device totally unusable.

That's just not possible in many parts of the world.

In real life, there is always this feedback edge from the results to the methodology.

Theoretically it's unscientific to do tweaks like this but in reality this is what actual science is because you need to see the results understand the problems in your experimental designs.

Now the interesting thing is that you could repair the bias problem. The main issue is that you will do these tweaks after a bad result not after they look fine.

Maybe we could commit ahead of time that the experiment will be reanalyzed after results regardless of what they are. Instead of only when the results disprove the hypothesis.

So like artificial analysis committing to a fixed cadence of index updates instead of when the results start looking jank.


Its also available finally to Pro users! Just took 24 hours.

They gave out bankable resets for every day people on pro plans didn't get Astra. Given that, I wish they'd waited a few more days before activating it on my account :-D

> They gave out bankable resets for every day people on pro plans didn't get Astra.

Yeah, when I saw that Tweet I knew the person was saying it because they knew it'll be available within 24h.


I must have been one of the last ones to get it because I managed to snag two bankable resets. Already reset once after having it clear up geometry in Blender, but it did a fantastic job!

They haven’t activated Astra for me yet, I have two resets now. I’ve been using the opportunity to test out how good 5.6 Sol is at computer use asking it to generate stuff in Blender which has been… interesting

Edit: nevermind it JUST gave me a notification to use it!


That's a pretty genius internal incentive to move fast.

Meanwhile Fable with it's restrictions is still only available on 100 USD plan upwards.

The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false.

> Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime

https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

They found several bugs and they have patched them. Lots of work going into making sure lean is sound.


Some argue that Lean breaks a few type-theoretical properties. See full discussion here:

https://github.com/rocq-prover/rocq/issues/10871


Are you guys just posting what you think might end being the link so you can farm upvotes or something?


This seems to be the announcement w/ the trust me bro numbers.

https://x.com/Alibaba_Qwen/status/2094968708288680276


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: