Problem is the stdlib is very small so proving even simple theorems still takes a lot more effort (for the AI) than in Lean. We need a mathlib!