Sam Altman says people may someday “buy intelligence on a meter” like electricity or water and critics say the vision sounds more dystopian than innovative.

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.

  • redhorsejacket@lemmy.world
    3·
    4 days ago

    I hate to hit you with such a tangentially related query to your main point, but what is “formalizing a proof”, and why is there such a discrepancy between the time it might take an expert (weeks if not months) vs an LLM?

    (It probably goes without saying, but my college career was spent in the Humanities, where there was not much emphasis on proofs, formal or informal, so I’m curious how the other half lives.)

    • spectrums_coherence@piefed.socialEnglish
      21·
      4 days ago

      There are proof assistants https://en.wikipedia.org/wiki/Proof_assistant that would encode a mathematical proof as code, and verify its correctness for you.

      Writing completely formal proof is very painstaking, because it means we will need to flash out a lot and a lot of details (which are mostly trivial for experts) for computers to accept it, and we also need to know how to work with proof assistants.

      Human proofs often ignore these details to make it readable, yet also make it more prone to mistakes. Whereas formalized prove in proof assistant can very rarely be wrong (unless there is an unlikely bug in the assistant kernel), but mostly unreadable (unless the proof is incredibly elegant).

      So in general, translating good human proof to computer proof requires more expert labor than huge conceptual innovation, yet it usually require the steep learning curve of understanding the ins and outs of a proof assistant, which can take years of experience.

      LLM used to be pretty bad at this because even filling in trivial details can quickly derail them. Recently a few flagship coding model are finally able to do this, albeit with a large amount of token consumption in thinking.

      • redhorsejacket@lemmy.world
        2·
        4 days ago

        Fascinating. My godfather is a mathematician at a local university, I’ll ask him whether this is something he runs into. I’ve heard him grumble about formatting his work in the past, but usually in the context of using Latex, which I gather is something else entirely.

        • spectrums_coherence@piefed.socialEnglish
          2·
          4 days ago

          Yeah LaTeX is a bit different, think about describing a process in MS Word, v.s. writing a program that performs such process on a computer: LaTeX is more like description aimed for human consumption, where as formal proof is more like a program that computers can rigorously execute.

          Proof assistant have only attracted the attension of mathematicians very recently, thanks to the organization surrounding MathLib in Lean, and the promption of Terance Tao.

          It also rides the AI train quite a bit, as AI have a tendency to confidently be wrong, having a computer to check its proof can be very useful.