Constructively efficient algorithms without efficient correctness and efficiency proof I am looking for natural examples of efficient algorithms (i.e. in polynomial time) s.t.


their correctness and efficiency can be proven constructively (e.g. in $PRA$ or $HA$), but
no proof using only efficient concepts is known (i.e. we don't know how to prove their correctness and efficiency in $TV^0$ or $S^1_2$).


I can make artificial examples myself. However I want interesting natural examples, i.e. algorithms studied for their own sake, not created just to answer this type of questions.
This is the same idea as Andrej's answer but with more details.

Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 &lt; y_1, y_2 &lt; x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. This gives a bunch of examples since any NP algorithm for primality testing basically yields such a $\Sigma^b_1$ formula. In particular, the AKS primality test gives such a formula (when appropriately recast in the language of $S^1_2$). The paper by Krajicek and Pudlak gives more cryptography related examples of this kind but predates AKS and related advances by a few years.