This article is an excerpt from Hartnett's new book about Lean. I'm excited to read the book, but not very impressed by this article.
Specifically, the story is fundamentally about collaboration, and to frame that as a story entirely about Tao is bizarre.
www.quantamagazine.org/how-terry-ta...
With automated proof-checkers, a problem can be broken up into small chunks, solved bit-by-bit, then reassembled with confidence that every piece is correct. For some, this heralds a new area in mathe...