cross-posted from: https://lemmy.world/post/47387000
Sam Altman says OpenAI wants to sell intelligence like a utility
During a recent appearance at BlackRock in Washington, D.C., OpenAI’s Sam Altman, shared his vision for the future of AI. At one point saying, “We see a future where intelligence is a utility, like electricity or water, and people buy it from us on a meter.”
Altman was describing a world where AI becomes a foundational infrastructure, something woven into everyday life so deeply that consumers and businesses simply “plug into” it the same way they rely on electricity, Wi-Fi or running water.



And how badly does it hallucinate while doing so?
That is the thing about formal proof: if the definition is correct, which usually is relatively short and should be written by human, there is almost no chance of the prove being wrong. The only exception are when the LLM exploits a bug in the proof assistant kernel, and these kernel are usually designed to be exceptionally small, thus making bugs unlikely.
That being said, opus 4.6 found a bug that eventually lead to the proof of false (opus is unable to produce the proof of false, hence unlikely to exploit it): https://github.com/rocq-prover/rocq/issues/21682
However, like I said, the code quality of the llm is usually not on par with an expert, and they have a tendency to produce unnecessary lemmas and complications that will need to be cleaned up by human.
Also, we have a very detailed pen and paper proof, which are designed to be easily translatable to proof assistants. We have also setup all the lemma and theorems to reach the end goal. All of these are done by humans, without these, I don’t believe any LLM can make much progress on this project.