I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the Lean libraries.

My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!