Can We Meet the Challenge?

Incrementally

• Generate theorems ...
• ... that are hard for ATP ...
• ... and interesting to humans ...
• ... and hard for humans

You Can't Cheat!