Re:Formalizing the proof of PFR in Lean4 using Blueprint: a ...
by laichzeit0 on Wednesday December 06, 2023 @12:07AM
(#38540652)
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.
[ Parent
| on HN ]
Re:Formalizing the proof of PFR in Lean4 using Blueprint: a ...
by t_mann on Wednesday December 06, 2023 @01:58AM
(#38541152)
It 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.