Proof-theoretic blowup conjecture

Gödel never proved that mathematics cannot be formalized, only that all of mathematics could not be completely formalized in a single recursive axiomatic-deductive system. Most of all mathematical theories can be formalized in a axiomatic-deductive system. This means that if the proof is not too large for present hardware capacities, a computer can find it. Most of the fundamental results commonly used in applied mathematics can be formalized in fragments of second-order arithmetic. There is no need for dependent type theory or axiomatic set theory. A computer can find all the fundamental results in mathematical analysis used in applied mathematics. Any result in mathematics, formalizable in a suitable fragment of second-order arithmetic, which has a proof not too large for present hardware capacities, can be in principle found by a computer.  Every part of mathematics applied to medicine and engineering that has benefited humanity can be formalized in second-order arithmetic and its results can be discovered by a computer.  But how can the computer deal with the unmanageable size of the search space for finding a proof?  Obviously by processing and translating the sum total of human mathematical papers and transforming them into proof search heuristics. Just as early Chess computers were based on all past games. Instead of searching for a proof, interpret first the theorem as a game.  Why not stick to second-order arithmetic and weaker systems and their metatheory?  Why not try to do more with less, not only do more but do better?  One can doubt the cultural and human value or even consistency of mathematics that depends on axiomatic set theory, dependent type theory and even category theory. There is such a thing as a finitist or a ultrafinitist. An ultrafinitist is someone who upholds not only the importance of computability/ constructability but also of feasibility. Someone who states the obvious. Hilbert's 24th problem. A new Gödelian conjecture: given any positive integer N, and a small but relevant and expressive formal system S (like fragments of second-order arithmetic), there exists a small theorem T in S such that the smallest proof (in the Hilbertian sense) of T is larger than N. We can also require the proof to be constructive. In this case NP-complete problems might be of interest.  What would be the ultrafinitist refutation of the neo-Gödelian conjecture? The problem with the conjecture is "small theorem T". We need a rigorous theory of "smallness" and feasibility (E. Nelson did this).  But we can reformulate:

Given a relevant and expressive formal system S (such as a fragment of second-order arithmetic) which is small enough to be formalized by a program P using current hardware, there exists a theorem T in S which is small enough to be inputted into P and such that the smallest proof of T is too large to be found and stored on current hardware.

A kind of proof-theoretic blowup or singularity theorem.

A better formulation. We call a computable function $f$ an explosion function for a stem S if for every natural number $n$ there is a theorem $T$ of S of length at most $n$ such the smallest proof of $T$ is $S$ is at least of size $f(n)$. 

The alleged mathematical and research papers released by OpenAI have not been peer-reviewed in reputable academic journals. Furthermore, only roughly half of such alleged proofs have associated Lean "verifications" and it still has not been checked if such Lean "verifications" represent correctly the results of the associated paper. Mathematics is not a game played in a single formal system. It is about using one formal system to prove metatheoretic properties of another - or to prove something about how one formal system can mirror or interpret another, etc. Mathematics is based on the meaning we assign to symbols and the postulates we accept in order to confer epistemic validity and power to the use of formal systems. It is possible that theorem is computationally intractable in one formal system but, having discovered the interpretability of this system by another, the theorem becomes tractable in the other system. Mathematics was never about brute force proof searching, but about metatheoretic mirroring and interpretation and philosophical postulation. Mathematics is not a game but the game of games.