Comment by EA-3167

1 day ago

The key here is that it’s depending on the human inability to connect the sum of relevant knowledge, but said knowledge comes from humans.

Theres going to be this field day of low-hanging fruit that ML can round up, but after that I suspect it will be in fits and starts as a “connection maker” rather than some proof producer.

I think we're underestimating just how much low hanging fruit there is. I've been trying to apply this LLM research process to physics (QM and solid state) and there is so much missing in Physlib and the rest of the Lean ecosystem that most of my work has been trying to formalize the theories and validating them against the specification problem (and mostly failing badly).

It's not only going to be "connection maker". If and when robotics advance to a point where the LLMs are embodied, they can run experiments in the physical world and find new knowledge.

  • Robots in labs already exist, but mercifully they're not hooked up to anything as unpredictable as an LLM. Robots tend to work best as specialists doing high-throughput, extremely repetitive tasks which nonetheless require a degree of precision. Giving a robot a "human" body makes very little sense if we're talking about the needs and productivity of a non-human; humanoid robots are marketing for humans.

    • Humanoid robots are obviously more than marketing. The entirety of human civilization is human shaped. Making robots that are human shaped is easier and more efficient than redesigning and rebuilding everything that exists.

      18 replies →