We chose a target domain for our Build Your Own Proof Assistant class today. We are going to build a very encouraging and friendly proof assistant for middle/high-school geometry proofs. Any resources or tips for targeting this domain?