Comment by andriy_koval

10 hours ago

especially compared to existing 129 pages proof by human

6 comments

andriy_koval

Reply
black_knight  8 hours ago

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

  • itishappy  7 hours ago

    A published formalization is code. I would not think humans have any edge when it comes to citing previously published results.

  • andriy_koval  8 hours ago

    > 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  8 hours ago

      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.