emily’s Reviews > The Proof in the Code: How a Truth Machine Is Transforming Math and AI > Status Update
emily
is on page 9 of 288
‘Some—like to do geometry using formal machinery that removes them from the shapes they’re thinking about. They know the shapes only as equations or other abstractions. Hales did geometry the way a child would—imagining bubbles floating around in his mind—learned about the Kepler conjecture—tried to solve it as a hobby—sketching how spheres move around in relation to each other—slept less than five hours most nights’
— Sep 16, 2026 06:53PM
Like flag
emily’s Previous Updates
emily
is on page 72 of 288
‘Most questions mathematicians care about cannot be expressed in their language—In practice, this means computer science & mathematics have different standards for settling questions—For those who remained on Slack, he set new expectations: If you wanted to be listed as a Lean contributor, you needed to act like one—If you found a bug, the first step should be trying to fix it yourself, not immediately flagging it—’
— Sep 22, 2026 05:10AM
emily
is on page 36 of 288
‘—he had—intuitive sense that it was difficult to define what ‘beautiful’ meant. Was that painting really beautiful? &—how could one know for sure? These—subjective claims made him uncomfortable—Even in math, seemingly as objective a pursuit as exists—taste determines what kinds of problems are considered important to solve. Mathematicians—talk about—proof of a new theorem as beautiful without being able to define—’
— Sep 19, 2026 05:14PM
emily
is on page 27 of 288
‘A gap in the logic of a proof is like a bug in software code—Human beings bring experience—intuition to the process—Writing a math proof in a formal language a computer can understand, by contrast, requires defining every term—every step—& if one skips a step in a formal proof, it doesn’t know where to go next—It was a lot of time against the scale of a human life, but he was ready to commit it—had no other choice.’
— Sep 18, 2026 06:55PM