Abduction: Abduction Prover against MiniF2F

[yutakang]

• Domain-specific optimisations?
  • [ ] Avoid template-based conjecturing when no user-defined types appear in the proof goal.
  • [ ] More tactics for math problems.
  • [ ] math_olympic mode or IMO mode
  • [ ] How to handle large terms?
  • [ ] Local assumptions and fixed variables?