We recently released a set of 10 mathematical statements in arxiv:2602.05192, with known ibut unpublished short human proofs (about 5 pages), and attempted to ascertain how far AI systems can go in autonomously proving them. I will discuss why I think this exercise is interesting, what the outcome was from different systems, and some preliminary lessons from the results.