- 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 `fix`ed variables?
fixed variables?