A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.
replyWouldn’t a lot already be in leans mathlib?
replyA published formalization is code. I would not think humans have any edge when it comes to citing previously published results.
reply> I am sure a lot of this development was formalising the prerequisites
replyHow can you be so sure its not result of inefficiency?
Oh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies.
replyI have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.
Insert meme with 200 pages needed to prove 1+1=2 rigurously
replydeleted
reply