Jesus Margar on Nostr: Everybody working in this subject knows who Tao is. I've read his thoughts on this ...

Everybody working in this subject knows who Tao is. I've read his thoughts on this before. The reason I'm sceptical is because the bits we need help with in many fields are not symbolic computations. By the way, Lean does not do symbolic computations, it verifies proofs. The article claims the LLMs will be able to come with bits of the proofs themselves to input into Lean but they'll do that by basing it in other proofs. That's not how good papers are written: you need new ideas.