Some things we'd like students to do for us, because our time is limited, and they're not bad starter projects:

Undergrad/Masters

Proof Checker GUI via Sidekick

What I want for the proof checker can be explained succinctly, so I'll do so. Here it is:

I'd like to be able to right-click on a subterm of the entire term and see the various things that can be done to it. As examples, in this right-click menu, there would be an "expand" option, maybe a "contrapose" option (if appropriate), a "rewrite" menu that would expand to show the names of possible lemmas that can be used for rewriting (and mousing over on each name could show the information that show-rewrites currently displays). I could then choose something to do, and the display would be updated accordingly.

I suspect that professionals and students both would use the proof checker more if it could be more easily used. I know there are emacs keybindings for diving into forms, and the proof checker is very well documented. But, unless I use the proof checker on a weekly basis, it's difficult for me (a mere mortal) to remember what options are available to me when I'm looking at a term.

On the other hand, maybe trying to use the proof checker is the wrong idea, and I should just focus on taking advantage of the waterfall. Regardless, I think a GUI for the proof checker would be a great teaching tool for CS313k.

System Function Guards

See https://github.com/acl2/acl2/wiki/Ways-to-contribute

Github Issues

See https://github.com/acl2/acl2/issues?q=is%3Aopen+is%3Aissue+label%3AStarter

PhD

Parallel Interaction with the Theorem Prover

• When proving a function, explore the possible theory in parallel.
• Run accepted proofs in the background to see if there are events that can be disabled for each theorem, speeding up the proof or minimizing its dependence upon runes.

Also see the conclusion and future work section in Rager's dissertation. http://www.cs.utexas.edu/users/ragerdl/papers/dissertation/dissertation.pdf