A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.

> I am sure a lot of this development was formalising the prerequisites

How can you be so sure its not result of inefficiency?

	▲	black_knight 23 minutes ago \| parent [-]
		Oh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies. I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.