Finished reading two books in quick succession. They had one common area that linked the two together.
Author talks about Leo de Moura, an engineer working for Microsoft, starting a project in the early 'twenteens' to automate testing the correctness of software. Initially started as Z3 in the mid 2000's as a non-interactive version, it then evolved distinctly into LEAN (to mean keeping it simple). On the math side, it had predecessors such as Coq, and Automath. Though de Moura started the project as a software verification initiative that will help Microsoft, Lean was adopted first by mathematicians outside the company. Hartnett starting out the book with the story of mathematician Tom Hales solving the Kepler conjecture (that dates back to 17th century) in the late 90's helps readers understand the need for Lean like theorem provers. This is because his proof, submitted as a traditional math journal paper for peer review, struggled for a decade to find ink. The traditional peer review process didn't work well for that paper, since the math & the proof were too new that reviewers couldn't understand.
When Lean came into the scene, famous mathematicians started different projects leveraging the automated tool. For example, Hales gave up on the review process, used a theorem prover that existed then, called HOL to get the proof properly verified. Having realized the value computers can bring in to speed up theorem proving, he subsequently became a prominent advocate for Lean. Since the Lean project was handled solely by de Moura, who did all the coding, support, evangelizing, responding to bug tickets, Hartnett spends time explaining how annoyed de Moura was about the math world, endlessly complaining about features that didn't work well (as they were still under development by just one person) and asking for many new features. But later he understands their enthusiasm, supports them and releases versions 1.0, 2.0, 3.0. Latest version is 4.0, used by thousands around the world. Since the product wasn't being used inside Microsoft or outside for software testing, it wasn't generating revenue. Hence de Moura was perpetually on tender hooks, quite worried about his performance reviews, whether MS will continue to support his pet project, and will he ever be able to put it to use for SW verification. While such struggles are unfortunate and certainly stressful for him, it is so nice to hear about mathematicians starting new projects in subsequent years, with PhD students and post-docs around the world, jumping into collectively contribute to get projects to completion quickly. This helps setup working models that are new to the world of math, where multiple people geographically spread across the world work together! Usually such chronicling will be done decades after the projects were completed, and so the meeting of the minds discussed will all be in the distant past. Since Lean development is all fairly recent, meetings and conferences being described are just an year or two ago, to at most 20 years ago. This aspect was amusing while we go through the initiative's milestones!
One complaint about the book I heard is that it makes a Demigod out of Leo de Moura, without acknowledging all the help/work the community provided. I didn't feel that while reading the book as many mathematicians (Terry Tao, Jeremy Avigad, Kevin Buzzard, and Peter Scholze, to name a few), CS professionals, grad students from multiple countries around the world are all being talked about enough. I am reminded of a HBO documentary about the Chernobyl disaster, that combined 100s of engineers who worked on containing the damage into one female engineer to make story telling easier. While it works well for movie making, it does leave out the credit due to all those engineers, limiting it to a footnote at the end of the 4 hour long documentary. I can't say Hartnett uses that troupe at all. I can keep writing more, but will stop here, encouraging all the CS friends receiving this email to check out the book and try out the LEAN ITP, as it is a free open source software. If you are already using Lean, let me know how/where are you using it.
It’s an interesting gimmick: the book moves from a historical overview of AI into speculative sci-fi about how unconstrained AI might evolve. The historical recap (from the 1956 Dartmouth Conference, Marvin Minsky to various AI winters) felt a bit repetitive to me, as I've read about those milestones enough along the decades. But I think for youngsters who may not know about these developments, this might be a quick and easy primer. Since the book was published in 2020, the author’s near-fanboy enthusiasm for Elon Musk stands out on almost every page. I wonder if he would tone down the eulogy a bit if he were publishing it today!
Some logical projections author makes into the near future are neat. For example, if AI can accurately predict our daily needs and order items in advance, it could eliminate so many things that shape our zeitgeist, such as retail storefronts, marketing campaigns, most advertisements, and eye-catching product packaging (since an AI buyer cares nothing about colorful boxes). After titling the book as The Fall of the Human Empire, you'd think the author would describe the 2040 future as one in which machines fully subjugate humanity. Instead, the book concludes with humans ultimately pulling the plug on AI, relegating Lucy to a museum artifact that narrates the history of AI’s rise and containment to visitors. That makes the title feel like marketing bait-and-switch. Perhaps the author wasn't quite ready to take the dystopian premise to its logical extreme, choosing instead to acquiesce to the idea of human being continuing to reign supreme!
No comments:
Post a Comment