I see, with that mapping your original paragraph makes sense.
Just want to note though that such a mapping is quite weird and I don’t really see a mathematical justification behind it. I only know of the Curry-Howard isomorphism as a way to translate between proof theory and computer science, and it maps programs to proofs, not to axioms.
when translating between proof theory and computer science:
(computer program, computational steps, output) is mapped to (axioms, deductive steps, theorems) respectively.
kolmogorov-complexity maps to “total length of the axioms” and time-complexity maps to “number of deductive steps”.
I see, with that mapping your original paragraph makes sense.
Just want to note though that such a mapping is quite weird and I don’t really see a mathematical justification behind it. I only know of the Curry-Howard isomorphism as a way to translate between proof theory and computer science, and it maps programs to proofs, not to axioms.