If intuition is successfully used in proving a theorem (i. e. in producing the finite set of steps of a concrete proof), this demonstrates that the(?) mental model is generic (hence vague) enough, to cover important aspects of all models of the axioms involved in the proof. Or the other way round: The axioms are specific enough to cover important aspects of the mental model(s). But there is no reference to reality in this. Reality comes in by forming intuition.
If AD would be used to prove a theorem to predict sucessfully the behaviour of the stock market, the next generation of mathematicians would find AD intuitive (recall the history of Euklid's 5th postulate and the intuition about the geometric nature of space).
Ingo Dahn