I can't say whether I'm an idiot or not but, indeed, my background is in logic programming, first order logic and automated theorem proving (and other fields, not related to our discussion). Thus, I know that there is no formal concept of "proof" in logic. Even in automated theorem proving we formally define derivations, or deductions (which can be represented by the "mathematical objects" in your comment), but not proofs. As far as I know there is no mathematical or computational procedure that can construct "a proof", only arrive at a result that can be considered a proof, when the result is inspected by a human mathematician or computer scientist.

The concept of "proof" is, to my knowledge, only an informal concept, that only makes sense, and is only communicated, between humans. In mathematics that is even more so than in computer science. Certainly I wouldn't expect any expert on logic and proofs, to say that proofs "Just are". That sounds mystical, practically Platonic.

To give a concrete example (and you will excuse, I hope, my penchant for rhetorical flourishes, or at least terminological clarity, when I speak of the matters of my expertise) in Resolution-based automated theorem proving the derivation of the empty clause during a Resolution-refutation of a goal clause can be considered as a proof-by-refutation of the complement of the initial goal. That is so because we know that, if a set of clauses, Π, is unsatisfiable, then the empty clause is a logical consequence of Π. Therefore, if we can derive the empty clause from the union of a goal, G, and a set of clauses, Σ, we can assume that G is false, with respect to Σ (or, more precisely, that G is not a logical consequence of Σ) and that, therefore, ¬G must be true. We can do all that because we have fuzzy, human-readable proofs that convince us of the relation between Σ and G, and the derivation of the empty clause from their union; for example, in the Resolution theorem by J. Alan Robinson [1]. It would not be possible to set up an automated theorem proving system without such a human-readable, and human-convincing proof. Because nobody would trust it.

In fact, the Resolution Theorem, essentially a statement of the soundness of Resolution, is a statement of such irrefutable simplicity that there can be no doubt of its truth and, as far as I know, it has only been proven once, by Robinson, then his proof cited by anyone else interested in the matter. The completeness of Resolution on the other hand is more complicated to show and there have been many different proofs of it, in different forms (i.e. the Refutation-completenss of Resolution, and the Subsumption Theorem, proved by Robinson and others in different ways). Given that there are now many different proofs of the Completeness of Resolution, arriving at it from different directions, we can also be reasonably secure in the knowledge that Resolution is complete. We may still be wrong. Some proofs have been shown to be wrong [2].

That is how proofs work in practice.

I commented to help you understand where you are wrong, and because I, in turn, was "triggered" by your arrogant insistence about things you clearly do not know as well as you think you do. I suggested you do a bit of reading to avoid polluting our common space on HN with bullish ignorance. You reacted with offense. That is a natural reaction, and I have experienced it myself, but I hope that you can nevertheless take something useful from our exchange. I have studied long and hard to acquire the knowledge that I have and I consider it my responsibility to share this knowledge. Perhaps I should refrain from doing that in the future though, if it ends up being more "triggering" than informative.

________________________

[1] A machine-oriented logic based on the Resolution principle, J. A. Robinson, journal of the ACM, Jan. 1965.

https://dl.acm.org/doi/10.1145/321250.321253

A text that I recommend to anyone intersted in automated theorem proving, and proofs in general.

[2] https://homepages.cwi.nl/~rdewolf/publ/ilp/ilp95.pdf