|
|
|
|
|
|
by treyd
4 hours ago
|
|
|
I don't think you understand the workflow. Terrence Tao has done a lot of work using them in conjunction with LEAN. You aren't having the AI check the proof, you interactively work on the same LEAN proof, handing off between the AI assistant and having LEAN check it and provide feedback for both of you when there's a mistake. |
|
|