Thirteen million lines in the margin: what makes this the good case
Claude formalized the first computer-checked proof of Fermat's Last Theorem in eleven days. The theorem is not the interesting part: that domain had a cheap, independent, hostile …
•
8 min read