“You’ve got to start with the customer experience and work backwards to the technology. You can’t start with the technology and try to figure out where you’re going to try and sell it.” — Steve Jobs
Lean lets mathematicians treat mathematics as code—break it into structures, theorems and proofs, import each other’s theorems, and put them on GitHub. The big idea is that eventually much of the humanity’s mathematical knowledge might be available as code—statically checked, verifiable, and composable.
The result defies mathematicians’ usual intuitions about what functions can and cannot do.
“There was this inescapable sameness, in a way. No matter what I did, I was in the same place doing mostly the same things,” she said. “I was very isolated, and nothing I could do could really change that. I’d wake up on certain days and realize, I’m just older.” Math became a kind of escape, a space that felt expansive when her daily life was not. “Mathematics was another world I could explore. A world that was not confining, a world I could access at any point just by thinking about it,” she said. “That’s how I grew up, thinking about mathematics as this world of ideas that I can explore on my own. That sort of process helped me see math differently than a lot of people.”