Hmm, I think it comes down to what the definition of "testing" and "attempt". A human will generate many ideas, and eliminate them without creating full proofs, by just seeing that the idea is going in the wrong direction.

It sounds like AlphaProof will doggedly create full proofs for each idea.

Is what the human is doing testing attempts?