3 ms·
Any chance this could be implemented for automated proof synthesis? Would love to see this used in F* or Lean.
by krapht 9y ago
Any chance this could be implemented for automated proof synthesis? Would love to see this used in F* or Lean.
- suryabhupa 9y agoTheorem solving is very closely related to program induction (we just change the grammar). Just as with Python, the underlying search space would be incredibly large, and while in theory, we could simply change the DSL and it should work, it'll probably involve a few more iterations of the model or other insights to see this to fruition (but it's definitely not impossible).