First of all, this is an amazing result. Second, I'm not too surprised, given all what has happened before. The thing is: LLMs are not grounded in reality enou

First of all, this is an amazing result. Second, I'm not too surprised, given all what has happened before. The thing is: LLMs are not grounded in reality enough as much as we are. Using Lean is exactly what that is: grounding LLMs in reality. We have (at least) 30 FPS vision, and can detect 5 ms audio delays, we do that in real-time. LLMs have access to some images and large amounts of text. Their propensity is to predict the next token. So the propensity to be additive and just say something (aka predict the next token) is higher than predicting something to stop. If LLMs would have: - 30 FPS vision - similar hearing ability - an ability to feel their lived experience - consequences to their "life" They'd be making more intelligent decisions than they are doing now. Simply because they have more context. Because in this sense, we have a lot more context than LLMs. Yet, I see people sometimes treating them as if they are at the same level as humans because their intelligence is similar. And that might be true, but where they get their data from is vastly different. Given our tasks, they are at a disadvantage. They need to sense more of reality. Have fun sharing the room with these digital intelligences. Given the topics they can consume, they are already better generalists than any individual. I might be wrong of course, I'd love to meet any individual that's a better generalist than an LLM.