Comment by Syzygies

LLM's are an extension of us. We sometimes have to work to learn something new; so do LLM's. It's all in how we manage that process. Reifying information is the whole ball of wax, what separates different people's success rates using AI. AI is more surfboard than self-driving car; you don't just tell it which way to go.

I still can't get AI to code well in Lean 4, but I'm writing a parser for a language that doesn't exist. AI understands the language as well as I do.