They exceed us in a sense. They can generate the kind of proofs that a computer scientist could love: it doesn’t matter how elaborate, long, or obtuse the proof is as long as the checker says it holds. Many proofs that people consider elegant and have expanded human knowledge tend to have qualities designed with intent for an audience to communicate the idea, motivation, and result. They exceed us in the sense that Alpha Go exceeds most players of the game.