For the record, proving the pigeonhole principle in Coq is sufficiently doable to be a mere four-star textbook exercise (http://www.cis.upenn.edu/~bcpierce/sf/current/MoreLogic.html). No exponential explosion of terms required!

>The problem is that you need to sample efficiently from the posterior distribution, and for anything AI related, MCMC isn't going to cut it.

Which is precisely why so much of the actual research work in probabilistic programming is to add more and faster inference strategies. One paper already got a 600x speedup just by using some techniques from the compilers/VM world related to caching whole and partial computation traces.