A year ago my judgement was that I had wasted my time on trying to work with the models and doing things myself would have been more productive as I would have gained intuition from the failures. Now it definitely seems to have figured out stuff that would have taken me more time than I have to spare on this problem...
Being a theory builder more than a problem solver I am excited for the future.
Also excited for fully formalised mathematics to hit main stream!