3 ms·
I find his comment on Copilot to be enlightening. He says it’s not always right, but he still finds it useful. Kinda like that old saying in stats “all models a
by laichzeit0 3y ago
I find his comment on Copilot to be enlightening. He says it’s not always right, but he still finds it useful. Kinda like that old saying in stats “all models are wrong, but some models are useful”. Language models are really helpful when you have enough experience to be able to judge when it fails, I do feel sorry for novices who don’t have enough experience yet to do that.
- t_mann 3y agoIt arguably matters a lot less in this context - you don't need experience to see when Copilot has failed at Lean, the compiler will tell you anyway. But I'm not saying that understanding it yourself won't matter. In fact, I wouldn't be surprised if the gap between him and more mortal mathematicians actually widens with the availability of those tools.