alt Hacker NewsThe 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.
Replies
putlake • yesterday at 6:32 PM
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.
➕ show 2 replies
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).