|
|
|
|
|
|
by spolu
1593 days ago
|
|
|
Copilot actually knows a bit of Lean and can be helpful when formalizing stuff. But it does not get the critical feedback we get from the formal systems (as it's not designed for formal systems). It would be interesting to eval copilot on the same benchmark as I'm pretty sure it can close some of the proofs still. |
|
|