|
|
|
|
|
|
by AIPedant
331 days ago
|
|
|
Most proof assistants do a good job with autogenerating a (deterministically correct) proof given a careful description of the theorem. Working on integrating this into mainstream languages seems much more worthwhile than training an LLM to output maybe-correct proof-seeming bits of text. |
|
|