thibsrn

I totally agree, and if you asked consumers, most would care and prefer for their smart home devices to communicate as little as possible with the outside world. And yet the market keeps offering invasive products, the discrepancy is frustrating.

There should be a system like the nutritional information on food and beverage products, as time went by most people read those and choose accordingly, which then incentivize companies to adapt their offering. We could imagine something similar which would define clearly the capabilities of the hardware or software sold, clearly labelled on the physical package or on the online shop with an easy classification for consumers to understand.

Now we are all wondering if it's once again one the big players training their models. They should be held accountable in some kind of fashion, it's weird that we accept that businesses gets attacked by an AI and nothing comes out of it. Sure, OpenAI and Anthropic are not intentionnally doing it, but they choose how much effort they put into building guardrails and sandboxing. They have no incentive to adjust their methodology if they are not sanctioned.

I wonder if the targeted businesses are compensated privately without the media and greater public hearing about it. Imagine designing and building weapons, which you use on the street to calibrate and test. "Oops sorry, this bullet wasn't meant for you".

Absolutely, I'm just saying it's better to focus political energy to counter the cuts specifically, to mitigate the damage of the current administration.

Even though I'm sure it's factually true that there is a decrease in interest from international young researchers to come to the US, articles like this are always a bit dramatic and have a political bias. More problematic are the budget cuts than the decreasing flow of talent from abroad. The country has enough domestic eager brains and the cultural capital to compensate later for this temporary dip.

How much information is there out there about official financial documents and audited (not self-declared) operational performance? It seems we are getting a second Tesla stock, where any financial multiples is under the market average because asset managers and individual investors want to hedge themselves against missing out.

In a way those equities act as stores of hope, where investors unconsciously agree to value them as if the ideal future path where all the promises are true is the one that will happen. Whereas they are more rational and have a balanced view towards other equities.

This article is not saying that AI did the proof magically. Their statement is quite clear, the agent system helped human experts for the proof, going back and forth at different steps. The complexity came from the size of the codebase and the compiled implementation, which an AI-assisted process was able to tackle at much greater speed than a meat-only team of experts would have. The experts are still responsible for designing the mathematical specifications, and maybe along the way something was wrongly designed, but I still feel much safer about Signal's architecture and implementation.

Great, what a great use case for AI. I feel like Google has been the cleanest of the big players in terms of useful contributions and control of their AI systems. This new proof agent doesn't seem to challenge the spec though, just the implementation, if I've understood correctly.

I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.

Thank you for sharing, it is a really interesting read. It expands on the different approaches that try to explain individuals' behaviors in a group. It is always good when there is some variety on HN and we get a bit of social sciences !

I don't know if there is a common API standard from a technical point of view, but there is the legal framework for it. Banks in the the EU have to provide an access to third parties who provide account information services to clients (themselves being regulated and supervised by a national agency). I would assume because it is mandatory, it is in the interest of banks to share costs and provide a single unified technical API, since they all have to spend the money anyway.

The title sets a lot of blame on the bank, but there might be other factors at play. It is possible that either national or european regulations or laws makes it mandatory for the banks to comply with a set of security features that makes it impossible for them to offer services to degoogled phones. There might not be any alternative because it would cost too much money to develop and more importantly to distribute it. It can also be the case that Google uses its influence over the android open source project to make sure it will never be the case.

There is a lot that is added to the prompt to lower friction, which in a lot of cases is really useful even if the user doesn't realise it. I think an Anthropic dev explained somewhere else in this thread that they added it for the model not to try to hallucinate your idendity when committing on git.

It's the same thing with web browsers. The browser adds my preferred language and operating system to the user-agent header, this way I can access the right content and download the right version of software quicker. I wouldn't want it to share my social security number but some sharing is alright to me. The problem here is people didn't know it was happening.

The model has no judgment or common sense, it has no idea that sending the email address would be a problem. I don't want it to come back to me when it's building software and gets stuck on something, I expect some independent troubleshooting and to power through, which it did in this context by adding the email address in the request. This is solved by setting the model instructions correctly, the problem is we don't know when it is going to try some new problematic behavior like this.

I don't know about other people, but my experience with Anthropic's products outside of the models themselves has been atrocious. The models are really good obviously, and have changed how all of us work, but their client software, be it Claude desktop, Claude on the web and Claude Code is bug-ridden, with an incoherent feature set and invasive behaviors.

My use cases are mostly analytical work, document generation, and code generation and review.

I used to have the Pro subcription for Claude but switched recently to the equivalent Plus subscription for ChatGPT. With Anthropic, you cannot access their inference servers without going through one their client software or paying the API pricing. It is really annoying as those are two different product categories and I'd like to use the client of my choice with an LLM. OpenAI allows you to do that, so I have a proxy running on my computer which connects to OpenAI's servers in the back ground and serves locally a Chat Completions-compliant API, with the requests counting towards my subscription.

I also have an OpenRouter account, I use it regularly but mostly to explore new models and see what's out there. I wish I used it more but the bigger part of my requests, almost all of them, go through my subscription. My thinking is since I'm already paying for it, might as well use it. Which is a shame because it prevents me from exploring more.

I even think a combination of the free tier of Big AI with a pay-as-you-go pricing for more complex requests would actually be cheaper for most people than their current subscription, even with their heavily subsidized pricing. The problem is that most people wouldn't want to think of when they should go deeper with a bigger model and wouldn't want the mental task of switching. The same way people don't really switch thinking levels with a given model, even though it would be a more optimal use of their token pool.

There is a huge market for an alternative business model around LLM inference. The big providers will obviously go towards an ad-based model in the following years, which will be good enough for the greater public, but a lot of people and small companies would be interested in packages and subscriptions that suit their specific needs and lines of work. OpenRouter has a great product and there is so much possiblity in this space. I also believe there is so much potential in the development of models based on data primitives other than text or rasterized images, which would be really useful in a lot of industries.

For the frontend, I either use the web-based version of ChatGPT for quick questions and analytical work (the desktop version is unnecessarily heavy), or Open WebUI. For coding, I mostly use Zed. I like the traditional development environment and tooling, I tried several agent-first environments, but in the end I prefer an IDE on top of which agents were added. OpenCode Web has evolved a lot, I have been using it for quick scripting as well. I never use any coding agent TUI anymore. Behind the scenes, the agent harnesses are OpenCode and Codex. I use them interchangeably, I don't see much of a difference. Zed connects to OpenCode and Codex through ACP. Both OpenCode and Open WebUI connects to OpenRouter and the OpenAI Proxy. Open WebUI has Open Terminal, which I have been meaning to explore, for there to be less friction between any analytical work and a document that would be needed to be produced out of it. I also run small models through llama.app from time to time, when I want to be reminded how weak my computer is.

I don't use any orchestration tool. I don't have any work that involves so much volume that it would require that kind of setup. It's more important to me to maintain the right mental model, I don't want to risk any discrepancies between what I'm thinking and what's done. Therefore the agentic work must be single-threaded, if that makes sense. I also don't use AI chat gateways like OpenClaw or Muse because I don't want to do that work on my phone every minute of my life. I'm either working or I'm not.

This comment is longer than expected. It's such a fascinating and still evolving space.