From an neo-intuitionistic point of view based in Kant's assumption that space and time are aspects of human thought rather than reality (whether or not you follow down Brouwer directly in finding all negation questionable) mathematics is not an objective description of some conceptual world, it is an exploration of shared human intuitions and how far they can be leveraged by combination among themselves. It is, in that sense, the oldest branch of rational psychology, if it is a science at all, and not a privileged branch of the sciences that happens to be 'exact'.
From that point of view, I would argue that correctness is, at base, an emotion, a feeling of accord with intuition. Especially in the case of mathematics, we are seeking to express how a set of intuitions aligns, and not any actual fact.
We codify various parts of mathematics that we have agreed capture an intuition in a checkable form. But the codification itself is only going to become a community norm if it appeals broadly enough to a certain cultivated emotional response.
We are obligated to accept combinations of things already proved into new things only because we feel we should, and because we have assented to basic logic giving the rules of combination. If we cannot get the impression that we have seen the connections between the things combined, we do not agree.
Even if someone can, we are attempting to isolate shared intuitions, so from this point of view, we want enough people to weigh in for us to trust that these are not mistaken or idiosyncratic examples. So no, a proof has to be vetted by a number of people, and found not just mechanically correct, but trustworthy.
Only a radical Kantian, like Brouwer would maintain that basic intuitions cannot conflict. And choosing to see intuition that way leads to the decision that things like negation and completed infinity are not intuitive, even though they keep showing up in simplistic explanations. They are still intutions, but they need refinement.
The fact that when you pursue some group of strong intuitions far enough they often conflict with other equally strong ones is not disproof of the notion, only its most radical form. The later forms of neointuitionism do see that intuitions conflict. And they look at what happens with mathematicians run across those places as proof they are right about what math is really doing.
We have, for instance Russell's paradox "Does the set of all sets that do not contain themseveles contain itself?" In that we can see that when we put them together negation, universal quantification and containment result in something illogical.
But solving that problem is still the analysis of the intuitions, picking and choosing between them or replacing them with other more compelling formulations. Zermelo and Fraenkel replace the notion of unbridled universal quantification with an exploration of what we mean by making up a set, Brouwer limits negation to what can be constructively validated, Quine and Lawvere reshape the notion of containment referentially or merelogically so that it is directional and things can only contain themselves in a more trivial fashion.
So we end up with the seeds of three whole branches of math from this resolution: Set Theory, Constructive Analysis, and Category Theory. But what was the goal? The goal was to refine one or the other of these intutions so that it could be freely combined with others. This is not the proof that intuition is not the focus of mathematics, it is evidence of the process of interrogating spatial intution in progress.
No successful branch of mathematics exists that is not, or at least was not originally, driven by the need to refine a given set of intuitions. Geometry and all forms of Analysis, even non-Euclidean geometry and function spaces, works from our views of space: the fact that you want to use only part of a complex of intuitions and combine it with other options does not keep them from being your focus -- and manifolds are all locally Euclidean for a reason. Algebra work from the need to refine our ideas of factorization of complex mechanisms into simple parts -- Group theory is not about operators, it is about the classification of groups by factorization. Topology is about the problems of what is an inside and what is a boundary, something that is intuitively relevant to us even if it never really happens in nature. Etc. etc. etc.
We like to pretend that all axiomatizations are equally valid, but in fact, we choose axioms that represent intutions, and when they fail to fit, or we decide that the intuitions they eventually conflict with are stronger or more important than the ones they model, we change them. And not looking at the success of various fields is silly. We do not say 'but all that unsuccessful physics is also physics', and the Formalist contention that random axiomatizations that do not capture any relevance and ultimately simply die are still mathematics is equally silly.