Is this in the same sense as "almost all numbers are not natural numbers", and if yes, then what good does this bring?
The real challenge would be to show that "interesting" programs (i.e. that generate some sort of real world data) are solvable. There have been similar efforts in the field of complexity theory that aim to show certain NP-hard problems are tractable in the case of real world data (as opposed to a pathologically selected worst-case problem).
Also, is your code for exploring Turing machines public? We could perhaps use it in our project (see my other comment)
My code isn't public at the moment. It's written in Julia and rather messy so I'd have to clean it up a bit, but I wouldn't be opposed to putting it on Github.
I really like your project idea btw. It never occurred to me that all that time and energy wasted on proofs of work could be spent approximating the universal distribution. That could be really valuable.
Most of the problems with sharing messy code are purely in the author's head ("please don't let other people know how terrible my code is") and once you actually bite the bullet and just push the code, it turns out to be like most secrets, really stressful to keep secret and actually not that big of a deal once everyone hears it.
And for the real code problems, the broken corner cases and unfinished tests, well, if you put it on Github someone else might fix it for you :-)
A lot of papers showing progress on computable approximations have been published just within the last year. There was one recently showing that the halting problem is in fact solvable for “almost all” Turing machines, which is a bit surprising; I would have not thought this was the case. Ultimately though, we don’t need to find the absolute shortest Turing machine that produces a given output string — we just need to find a decently short one that performs better than our existing models. Any sort of algorithmic approach is bound to be vastly superior to a purely statistical approach.