During class, we will divide into groups and discuss future work ideas. Some things to possibly talk about, if it helps guide the conversation:
- What do you think are some of the biggest outstanding problems in proof automation?
- Where has the work you've seen fallen short so far?
- What did you find most difficult about using the tools you've seen so far?
- What do you think is preventing proof assistants from becoming more widely accessible or usable?
- What ideas do you have for future work in proof automation?
- What do you anticipate some of the biggest challenges toward working on those ideas will be?
- What work you've seen so far may be useful toward solving these problems?
- What technical approaches might you take toward solving these problems?
- How might you evaluate whether you have solved those problems successfully?
With about twenty minutes left, we will leave our groups and spend about twenty minutes writing down our own ideas privately. This is to help give you a start on your elevator pitches for next week.