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.