Re: what is "software"

Are proofs that have never been written down or contemplated
by anyone real proofs? If they're not, then proofs about
proofs (i.e. in logic) are really proofs about proofs and
pre-proofs. This seems like something I would expect
ultra-finitists to bother with, but I don't recall ever
reading anything where they have. Of course, this doesn't
mean much, given how little philosophy of math I've actually
read. Most of this subject is pre-philosophy of math to me.

Dave L. Renfro (pre-trolling ---> trolling?)

And if proofs about proofs are really proofs about proofs and
pre-proofs, do some of them require refinement where pre-proofs are
concerned? In most cases, I doubt this is an issue. But I suppose it
could come up.

Also, could some proofs about proofs and pre-proofs be refined into
stronger proofs that are solely about proofs? Possibly?

.