Book recommendation: “The Proof in the Code: How a Truth Machine Is Transforming Math and AI” by Kevin Hartnett.

This is about the creation of the Z3 solver and how it drove the creation of the Lean programming language, such a fun and thoughtful reading. And the cherry on top is that Z3 was created by a Brazilian, Leonardo de Moura. In the WC mood, VAI BRASIL! 😀