Full Width 
Shortcuts 
Sign Up 
Log In 
Articles 
Reading List More from Shilin typing
Lately I've had a lot of time for thinking. Partially because I shut down Blymp back in January and freed up a lot of my mental resources. No clients to follow up with. No admin stuff to stress about. But thinking is also my favourite activity, and there'll always be time in my day for a good old mind-bending. So I sat down, as I often do, alone with my thoughts, and wrote about what business I should and, most importantly, should not consider doing next. The list you are about to read might be similar to Core principles I (try to) live by that I wrote one similarly pensive evening two years ago. Whether it's a comparison or a continuation is hard to say—still, one can't be without the other to show the inexorable passage of time that changed everything and nothing for me all at once. But it also serves another purpose: to remind me in the future, before I get myself involved in some dubious enterprise, what painful mistake I'm about to make by ignoring my values. So here it is, the list. My next business shouldn't (and hopefully won't) be about: Social Media. Enough of this crap. Some productivity bullshit. Do better, not more. Fast fashion and consumerism. Truly, I've already bought everything you wanted to sell me. Some “hack your health” app. Our bodies haven't changed much in the last three hundred thousand years, and they won't change in the next hundred. Or any other app, really. I don't even use my phone anymore. Distracting things and things that require constant attention. Some LLM wrapper with a fancy UI. Indefensible. The number of things I can do with ChatGPT or Claude is ridiculously high. It can surely handle one more thing. What it should (and hopefully will) be about: Sustainable, high-quality products Unscented products Building community Bringing people together, offline Empowering creativity Replacing animal products Doing one thing really damn well Small acts of kindness Things you can touch Things that last Clothes made of natural fibres Art Fun Questioning the status quo Simple, intentional living Deeper understanding of self Spending more time in nature Spending more time with loved ones Things and businesses I get inspired by: Framework: Sustainable/repairable laptops. Bitwarden: Open-source software that does one job really well and charges me a reasonable amount of money per year. Danish design: Beautiful. Sturdy. Timeless. I brought home two Royal Copenhagen mugs the other day. Bike-sharing and car-sharing. Literally anything-sharing. ZSA keyboards. What a keyboard should have always been. A water bottle that won't leak on a plane. Some random-brand bottle bricked my friend's MacBook, and I've been appreciative ever since of the fifty-dollar water bottle that I bought years ago, so hesitant about the price. Coffee. One of those timeless things on Earth. Kobo. It's like Kindle that doesn't decide what's best for you. Upload your own PDF. Or EPUB—whatever. It has physical buttons to flip pages. Best $200 I ever spent. A high-quality safety razor. It's just so nice to hold. A Japanese stainless-steel knife. So nice to hold, too. There are numerous other things that I appreciate having in my life that didn't make it into this list for some reason or another. A familiar mom-and-pop shop in my neighbourhood. A Timemore Black Mirror kitchen scale that just works, every time. A random USB-C charged electronic device that spares me from carrying an extra cable. My radically outdated ten-dollar Casio watch. An old pair of comfy shoes that just won't die. We need more of this in our lives. Things that you desperately look to buy again when they get lost or break or fall apart. Things that someone made a deliberate effort to get right the first time. The quintessence of art and craftsmanship. For all the genius of Steve Jobs, the iPhone wasn't that. It challenged the status quo and was surely a groundbreaking, outstanding piece of technology at the time of its first release. But in twenty years, people won't remember it ever existed. Like Gen Z doesn't remember the Walkman. I'd like to see more businesses that bet on doing one thing really well. Google could still have been the company people remembered for the best search engine if they had doubled down solely on that. Instead, we don't even know what they do anymore: Phones? Clouds? Ads? Certainly ads. I still remember the feeling of holding one of the first PocketBook e-readers in my hands back in Moscow. Pressing its buttons and waiting for what now seems like a torturous three seconds before the screen refreshed. Almost twenty years later and every day still, Kobo gives me exactly that feeling. So hopefully, my next business is the one that lasts.
Yesterday, I traded sun, beach, and a beautiful warm sea for a cold, gray sky and a pair of wet shoes. I still can't believe I did it. The constant winter overcast was reason enough to leave Canada and never look back. When I finally left, I had bought a ticket to a never-ending summer. It felt magical. Yet I am here in the cold again, and I couldn't be happier with my choice. I arrived in Marseille this morning. Dressed in light pants and a summer shirt, flip-flops on my bare feet, I stepped out of the airport. Cold rain got under my collar and ran down my spine. I held my small backpack over my head and ran to the bus station. There I bought a ticket to Aix-en-Provence. After four years of waiting, my France chapter has finally begun. I could, perhaps, write about this weird obsession that I’ve had with France for the last four years. About the language, que j’adore. The petit café I had this afternoon followed by a risotto served with the freshest baguette, as if it were the only way to serve risotto. But I’ll keep my message simple: don’t stop dreaming. It's not about some bucket list with three hundred items in it. Nor New Year's resolutions that you regret telling everyone about. But a childish, almost feverish “What if one day I…” sort of dream. Something that you are ashamed to dream of, perhaps because it's so silly or so trivial that you don't know why you should even bother. But you dream nonetheless simply because you can. I remember my first such dream. Back in school, I watched Sean Penn's Into the Wild. I'd never wanted to go to Alaska. And it didn’t seem realistic, living on the opposite side of the world. But it had planted a seed in the back of my mind until more than ten years later I landed in Fairbanks. And today, arriving in Aix, another itch got its long-deserved scratch. I walked into a grocery store and listened to the radio that reminded me of my favorite Café Montréalais on Spotify. I strolled the narrow cobblestone streets and pretended I was the main character of a new episode of Dix pour cent, filmed in Provence for a reason known only to me. It was a dream. But then again, I was living it. Be a fool. Dare to have foolish dreams. They might, after all, come true.
On December 31, I went to Wat Suan Mokkh in Thailand and registered for a ten-day silent retreat. I scribbled these notes on eight scraps of paper given to us for questions on days six and ten. Neither electronics nor diaries were allowed for “creative writing”. And because my writing isn't that creative anyway, here we go: Day -1 Day 0 Day 1 Day 2 Day 3 Day 4 Day 5 Day 6 Day 7 Day 8 Day 9 Day 10 Day 11 -- P.S. A ten-day retreat somehow turned into a two-week-long adventure and will likely take a year to process. But what an experience it was!
As I fought with my mother for the hundredth time over a reason that was silly yet too hard for her to understand, I concluded that this post was long overdue. While I had ninety-nine other chances to complain about my difficult relationship with parents, I kept postponing it, fearing that I would alienate all my readers, who seemingly belong to one of two groups: those with toxic parents and those who fail to admit it. Above all is an unspoken rule to not talk ill about family, for only a wicked person with a mind and a tongue of a devil himself has wits to appear ungrateful to his kin. And being ungrateful to one's parents is of the same level of madness as being ungrateful to one's entire existence. But arguing with my mother for the hundredth time felt like a drop in the ocean—if the ocean could fit in a teacup and the drop were the size of a meteorite. What makes it unbearable is both the fact that I am fighting with the closest and the dearest person, and that the fight itself consists of no solid argumentation whatsoever and is for the same reason as all previous fights—my mother's own insecurity. Neither this nor previous conflicts had any resolution, apart from staying silent for a week and then pretending we had never argued in the first place. But this time the teacup overflowed, and risking alienating one or the other or even both groups I've decided to cut all communication with my parents and, since nothing can be worse, write about it, too. Speaking about my parents, I'll mostly be talking about my mother as the relationship with my dad has been close to nonexistent after I'd moved to my university's dorm at nineteen. Like me, my father is a lone wolf. Most of the time he keeps to himself, and when forcefully pulled out of his bubble of comfort, he gets irritated and practically impossible to deal with. Growing up with a father who rarely showed any emotion beyond irritation left me with a sense of detachment and struggling to connect with others. The weight of his silence—his emotional absence—became too much. There seemed no way to make him happy and so I stopped trying. Nothing can describe better his relationship with my mother than the fact that they have no common interests, and the only thing the two of them don't mind sharing, it seems, is the seat of the toilet. For some unimaginable reason they found it the most practical thing to keep living in the same one-bedroom apartment that my grandma bought with her own money some fifty years ago; the very same place that my older brother and I grew up in, sharing the only bedroom while our parents slept in the living room; the place that has seen every repair possible, from floor to ceiling, and therefore every repair but one—the repair of our parents' marriage. "Children of emotionally immature parents have to learn the hard way that they are not responsible for their parents' happiness, security, or well-being." — Lindsay C. Gibson, “Adult Children of Emotionally Immature Parents” This sense of solitude—perhaps a cover-up for my father's loneliness—is the only thing that unites him and me. Despite my mother bringing up my and his similarities every chance she has, I can't imagine a person more different. Unlike me, he had decided to have children, and so he reaped what he sowed. Unlike me, he kept torturing my mother with his presence out of convenience of staying under the same roof. And unlike me, he kept cheating on his partner, her being my mother, and repeatedly coming up with lies that even a seven-year-old could see through. But even the ugliest of characters have as much good in them as they have the ugly, and so my father somehow kept the appearance of a kind and thoughtful and caring person. And that is as much as I can say about him, for I am lucky to hear his voice once every March when I call to wish him a happy birthday. Before I talk about my mother—and the complexity of her character deserves more than a couple of paragraphs—I will question the relationships with parents in general. Why do we give our family their own category as if they were a cast above all others? Like the socialite in a country with a corrupt government, we are willing to forgive our parents all crimes and harassment and humiliation simply because they appear to have authority over our lives. And who am I to live through the consequences of their choices? In his “Book of Secrets” Osho argued that there are two types of people, the logical and the emotional. But when did we decide to treat parents above all reasoning? Why do our relationships with family, unlike those with friends or partners, fall through the cracks of our mind and straight to the emotions? Instead of treating our parents based on logic and according to their actions, we treat them how we feel parents should be treated. But I am a logical person and thus reason must prevail. Barely distinguishing any status and hierarchy whatsoever, I put family into the same box as friends and colleagues and business partners. I do so because a parent must be a friend first and foremost, or what is that relationship without trust and acting in each other’s best interests? A well-working relationship benefits both parties. If one pulls the blanket, leaving the other in the cold, what is there for the other to catch besides a sore throat and sniffles? It's natural for humans to strive to be better, and so we must surround ourselves with people who help us grow. Nobody wants to wake up in the morning a worse person than they were yesterday. To the best of our abilities and the capacity of our knowledge, we look forward to starting a new day better off than the one before, as little as the difference could be, and aspire to do good. Out of five closest people, besides a husband or a wife and maybe two best friends, why do we make space for the only two, the dearest, who constantly talk us down? Forty percent of energy spent in blame and guilt-tripping is a heavy price to pay for being born. So why do we keep paying it? On the contrary, the right friend is not the one who supports every endeavor, though I wish everyone had supportive friends. No, this is enablement. In this case, you might as well surround yourself with five AI chatbots as LLMs excel at that. The right friend is one who knows when to encourage, when to be silent, and when to be a voice of reason, should you ever do something outrageously stupid. But take my mother, for example, for she is a fair parent but a terrible friend. First, I don't remember the last time she sided with me. When I was leaving Russia, she acted as though I betrayed the whole country. When I had quit my job, she reminded me with every occasion that I'd better find a new one soon. Now, that I am contemplating a ten-day meditation retreat, I suddenly appear to be joining a cult and will soon be out of home—not that I've had a permanent place in the last eight months—and enslaved and sent to a labor camp. As I discovered recently, my mother has an intricate ability to find the weakest spot in my thinking and exploit it viciously. She may as well have Spider-Sense because she always knows what doubts I have about myself even if I don't disclose it to her for exactly the reason of that exploitation. Take the meditation retreat, for example. As it is my first time going away to some distant temple in the middle of Thai woods, I, who is just a monkey with a worried mind, hesitated every part of that decision: being far from the city, being in the woods, being in a Buddhist temple, surrendering all possessions and technology to god knows whom, and spending the majority of the ten days sitting in silence. And as a normal human being excited about his adventure, I shared everything and in great detail with my mother, though withheld the questionability of the activity. To my surprise, it took long enough to trigger her anxiety, as she only came back to me after four weeks. Ah, did she come prepared! Suddenly I was watching interviews about a disappearance of a young Russian man—how convenient it is to be just like him!—in a Buddhist meditation retreat. The interviewer was a handsome journalist from a Russian government-owned TV channel which spread all day long no valuable content but propaganda. The interviewees, on the other side, were the disappeared person's village mates with thin white faces and under-eye bags so big and blue that a poor makeup artist couldn't hide with a centimeter-thick layer of a concealer. Because nothing can conceal twenty years of drinking vodka. "Trauma robs people of their sense of agency. Healing comes from reclaiming a sense of control over their own life." — Bessel van der Kolk, “The Body Keeps the Score” The main flaw in my reasoning as I can so far see is that of being disturbed by my mother's poorly handled projections of anxiety. Truly, isn't that what makes one a greater person if he can be above all verbal abuse and manipulation? It is my choice to be offended, or is it not? But logic aside, the abuse is most hurting not because of the words themselves but because they come from the mouth of the closest person. Another might argue that we must ignore our parents' mistreatment and take care of them as one takes care of an older person because of age. But tell me then, if I am given a choice to save one person from a devastating fire, first being my mother, her life as mediocre as it is, and the other a noble biologist or, say, a pediatric surgeon whose work saves ten children each year, who should I urge saving? As I've recently come to making an extra dollar and realizing that not all is needed for my humble living, I considered donating a chunk of it, for that is the easiest I can do, not knowing what other use is there for the money. With these thoughts I came to my friend and asked him whether I should send it to a charity like The Red Cross or back home to my parents. Family always comes first, said the friend with the parents by no means nobler than mine. But to make him think a second longer perhaps I should have asked a different question: should I donate to a charity that provides humanitarian aid to those affected by war or to the two people that enable the very same war by bringing food and clothes to the young boys in the Russian military? Wnen I last wondered if my mother finally gave away my guitar that hasn't been played for a decade, she said that they've got many instruments in the army and that she sees no other way to dispose of it. Not all donations are alike. The reason my mother has such a complex personality is that I never know what next she'll throw at me. At the age of eighteen, I was thus presumed by her to be dating a hooker, since only a hooker could take interest in me. Little did I know that prostitutes have better things to do than flirting around with broke teenagers. Today, I seem to be dealing with drug addicts and alcoholics, in other words a questionable company, considering my mother's loud concern with me steadily slipping into crime. As someone who doesn't smoke, drinks sparingly, and is highly cautious about drug use, the only crime I am guilty of is not leaving my parents' house sooner. "If your parents have unresolved trauma and emotional immaturity, it’s not your fault. You’re not responsible for their healing." — Shannon Thomas, “Healing from Hidden Abuse” But to paint a picture this dark is not to give my mother justice. Having raised two children in a household so tiny that even a mouse would feel restless, and with a cheating husband as a cherry on top, she made sure we were warm and fed and somewhat happy. My brother and I had clothes and not rags, our toys were simple yet they were toys still, and both of us were educated by the best institutions that a family of our class could afford. I thank my mother for gifting me a guitar on my thirteen's birthday. I was let alone to play it, and I played it for hours straight, until the music has become the essence of my living. It was also my mother who transferred me to a better school after the 7th grade—though it meant steep monthly payments—after noticing that I was bored where I was, among the ordinary unmotivated students. The new school boosted my confidence and gave me amazing friends with whom I'd shared many precious moments, be it on the school's premises or besides a campfire some five thousand kilometers away from Moscow. It was, however, my very same mother who'd later tried to pull me out of that school—as I was spending too much time there—and send me to the outskirts of the city to a beaten-up college that produced no other alumni than cooks and plumbers. Another sharp memory of mine is waking up in the middle of the night at the age of eight to sharp gasps for breath. Someone was being chocked, I thought. The bed was shaking, rhythmically, methodically, and I was shaken with it. Shocked and scared, I slowly discerned my mother’s face in the dark, and then, above her, the face of a stranger. My parents never traveled together—although I don't remember them ever trying—and that night left me pitying my mother. An eight-year-old must not be asked to bear a secret of an affair of his parent, but I bore it anyway as I bore my mother's other, bigger pain of not being given the life she wanted. Nonetheless, I now had two cheating parents which didn't make my childhood easier. I don't know if there's a protocol of talking to abusive people other than ignoring them. I doubt it. It does, however, become more intricate when parents are the abusers. My journey into understanding parents' psychology began with reading Lindsay C. Gibson's book, named exactly as it should be, “Adult Children of Emotionally Immature Parents”. I had first gotten curious by the title, thinking that perhaps I would better understand my distant and self-indulgent father. I was wrong. I learned little new about him. Yet in this book I discovered a whole Pandora’s box that was my mother. I have since recommended this book to many friends and all of them came back saying that they in turn recommended it to theirs. This time my patience is over. I make no space for toxic people and I my mother will not be an exception. I banned her on Telegram, and she is the first person I've ever banned. I have no intent on keeping it permanent—but neither do I plan to communicate with her soon. If, like me, you’re fighting the internal battle of dealing with difficult parents, don’t you deserve a break too?
More in startups
We Live in the Dependently Typed Future Now In the thirty-four days between the fourth of September and the seventh of October, the following things happened. Claude formalized Fermat's Last Theorem in Lean. OpenAI announced a finite-time blowup for the Navier-Stokes equations, found by ten thousand agents in eighty-eight hours, with a Lean formalization attached. A model proved Khot's Unique Games Conjecture. Another multiplied two integers faster than \(n \log n\), with an exponent improvement of \(2^{-182}\) (so maybe don't expect it in GMP anytime soon!). The rational Hodge conjecture fell for CM abelian varieties. Then OpenAI dumped 722 new maths papers on GitHub on a Tuesday. And it's only been a month. The question everyone is asking now is how long until the Generalized Riemann Hypothesis folds to the swirling pool of tensors? Sixteen months ago I wrote that the future of maths may be deeply weird, and then, welp, just like that we're here now in that weird future. And it's f'ing awesome. Somewhere in a data centre there is now, more or less permanently, a building full of accelerators working the truth mines at the frontier of mathematics, just like in Greg Egan's sci-fi novel Diaspora, tunnelling outward from the three axioms propext, Quot.sound, and Classical.choice, and hauling results back to the surface around the clock. OpenAI posed its model roughly four thousand problems at an average of three hours of thinking each, and that is the slow, artisanal, normie-friendly version. The industrial version doesn't stop. It will produce results faster than any human community can read them, many of them correct, some of them important, and a growing fraction of them inscrutable. True (for some twisted philosophical definition of truth), machine-checked, and understood by no one. Human understanding of mathematics is about to become a luxury good. Whatever else this world needs, it needs something that can tell the true results from the confabulated ones at the rate the models produce them, and right now that something is dependent types, namely Lean. Let me dwell for a moment on how strange it is that this is the shape the future took. I spent a good portion of my twenties around the London FP community, where dependent types were the thing we talked about over pints at the Crown Tavern in Clerkenwell (some of you will remember). Types that could depend on values, so that a function's signature could say not merely "returns a list" but "returns a sorted permutation of its input," and the compiler would hold you to it. Curry-Howard, the observation that proofs are programs and propositions are types, was the foundational north star. The pitch was always that one day we would write software against specifications and the machine would check them, and the reply was always that this was a lovely idea for people with tenure and no deadlines. Dependent Haskell has been "a few years away" for about fifteen years. Idris and Agda remained boutique. Software engineering still mostly runs on C++, prayer, and the occasional dark incantation. And then the dependently typed future arrived anyway, through the back door. Mathematics and reinforcement learning got there first. It turns out the killer application for a dependently typed language was using its typechecker as a reward function. A type checker is an oracle that says yes or no to a candidate proof with no partial credit and no opinions, and that is precisely what you need when you want to point a very large optimiser at an open problem and let 'er rip. The thing we dreamed about at the pub is now critical infrastructure at frontier labs, and every one of the results above is, in the end, a claim that a type checker returned true. Which is why we need better tooling, and we need it ASAP. The dependent type renaissance is here and the golden age of formalized mathematics is upon us, but the inner loops of these data centres now run dependent type kernels day in and day out, elaborating, checking, discarding, and retrying at breakneck speed, and the thing that certifies their output should run at the same speed. If the search runs at microseconds and the verification runs at minutes, the verification becomes the bottleneck, and bottlenecks in trust have a way of being quietly skipped. We should not be in a position where the most important epistemic question of the decade, "is this proof actually correct," is answered by whichever checker happened to be fast enough to keep up. Breaking the Mathlib Minute Barrier Just like the four-minute mile, which went from physiological impossibility to something club runners now train for, formal mathematics has had its own barrier for a while, which is type-checking all of Mathlib from scratch in under a minute. That now turns out to be quite tractable. nano-lean is a minimal, but complete, type checker for the Lean kernel language, written in Rust on top of my unbound binding library for doing efficient de Bruijn indices for binders. It reads an export of a Lean environment and independently re-checks every declaration from scratch (inductive types, positivity, recursors, quotients, universe levels, projections, structure eta, all of it). It checks all of Mathlib, 718,577 declarations, with zero errors and zero timeouts in 16.7 seconds on an Apple Silicon M5 Max. A surprising amount of that speed comes from not parsing text. The standard way to get declarations out of Lean is lean4export, which writes one JSON object per line, and parsing gigabytes of JSON turns out to be a large share of the cost of checking anything. So nano-lean's companion tool olean-export reads the compiled .olean files directly, decoding modules in parallel, about a hundred times faster than lean4export on a Mathlib-dependent library, and it can emit blean, a new binary format designed for fast mmapping. Blean is the same record stream as the NDJSON export, in the same order, with nothing left to parse. Every record is a compact postcard encoding, ids are implicit and dense, records only refer to earlier ids, and each expression carries its precomputed hash. The checker mmaps the whole file, tells the operating system it will be read once front to back, and decodes names, levels, and expressions straight off the mapped bytes into its term arena. There is no parsing step at all. The bytes on disk are already very nearly the shape of the data in memory, which is how you check Mathlib in under a minute. -j 1 -j 10 Wall time 57.4 s 16.7 s Kernel check 53.5 s 12.5 s Peak memory footprint 7.5 GB 9.2 GB The same trick works on the frontier results too. Here is nano-lean checking the full imported environment of OpenAI's Navier-Stokes and Euler proofs on an M5 Max. -j 1 -j 14 Wall time 83.58 s 17.13 s Kernel check 78.83 s 12.11 s Peak memory footprint 10.14 GB 12.29 GB Divide Mathlib's kernel time by the declaration count and you get an amortised seventeen microseconds per declaration. That is the number that matters, because it is the right order of magnitude for a checker that lives deep inside an RL-driven search loop, where it gets called hundreds of billions of times, instead of sitting at the end of a release pipeline. The entire library of human-formalized mathematics, the product of a decade of volunteer effort, is re-verified in less time than it takes to make an espresso. I also happened to have an m2-ultramem-416 lying around on Google Cloud (416 vCPUs and 12 TB of RAM, as one does), so naturally I pointed nano-lean at it. Yes, it breaks the two-second Mathlib barrier. But Amdahl's law sends its regards, and the curve flattens out hard somewhere past a hundred cores, as the dependency graph runs out of independent work to hand out. Mathlib, it turns out, is too small. I look forward to the day a future Mathlib, or something like Tau Ceti, grows big enough to actually saturate this machine. That's the real future! I wrote it to make a point about where the bottleneck has moved. The kernel is now the hot loop of a new kind of scientific economy, and hot loops deserve to be engineered like hot loops. The whole bargain of formal proof is an asymmetry. Finding a proof can take three hours of frontier-model thinking, or eighty-eight hours of ten thousand agents, but checking it should take microseconds. That asymmetry is what makes it reasonable to trust a result no human has read. It only holds if the checker actually scales, and with Fermat's Last Theorem now weighing in at five times the size of Mathlib, scale is no longer a hypothetical. Mathlib is the small library now. Caveat emptor, though. nano-lean is a proof of concept, built to show that it can be done with the right amount of low-level Rust-fu. That said, we do use it internally at OneChronos to check our larger Lean proofs of market infrastructure, which have grown quite excessive. It is nowhere near as trustworthy as the official Lean kernel, which has years of scrutiny, a community of experts, and every Mathlib build ever run behind it, and which takes around fifteen minutes to check the same library. The claim is narrower and, I think, more interesting. Checking at this speed is totally possible, so we should stop treating minutes as the natural cost of trust and start building checkers that are both fast and trustworthy. A future version of the Lean compiler could be as blazing fast as rustc or clang. The Shape of the Future In my previous post last year I predicted that mathematicians would come to look more like software engineers working through pull requests on GitHub than like Andrew Wiles toiling in his attic. The largest single release of new mathematics in history shipped as a GitHub repository, with a CONTENTS.md, a Lean library, a lean-toolchain file pinned to v4.34.1, and a promise that "corrections and revisions will be recorded as new versions." So, yup, that happened. I predicted that an AI system would be unleashed on a list of formalized open conjectures in an attempt to systematically push the frontier. Four thousand problems, three hours each. Check. I predicted a data centre tasked with the Riemann hypothesis that would come back after weeks with a proof no human could follow. What we got was the quasi-Riemann hypothesis, every Dirichlet \(L\)-function zero-free in \(\Re s > 7/8\), with a Lean page, which is the sort of near miss that would be funny if it weren't so unnerving. And the inscrutability has arrived on schedule. OpenAI released "reasoning summaries" for ten families, which turn out to be summaries of excerpts of reasoning traces, two removes from anything the model actually did. I joked that the million-dollar Millennium Prize might cover a hundredth of your GPU bill. The Navier-Stokes run reportedly consumed around 130 billion tokens. So definitely yes. What I got wrong was the timing. Last year I wrote "we're not there yet. Not even close." It was sixteen months. I probably got the chess analogy wrong too. I argued that, as with Stockfish and chess, machines would make mathematics more popular and more accessible rather than less. Maybe in the long run. In the short run the mood among working mathematicians is closer to existential crisis, and the open questions are about career pipelines, PhD students getting scooped by a press release, and the concentration of the most powerful mathematical instrument ever built inside a handful of private companies running unreleased models. What I missed entirely is that the bottleneck would turn out to be plumbing. I spent paragraphs on Gödel and the epistemology of inscrutable proofs, and the actual first-order problem is that the OpenAI Lean library is over a gigabyte of source across tens of thousands of files, and their README has a section warning that building it may fail because Linux's vm.max_map_count is too low, with a suggested workaround of recompiling Lean with -DMMAP=OFF. The philosophy is still there. But the frontier of mathematics is currently being held up by a kernel tunable. Which isn't the future we wanted, but maybe it's the future we deserve! Who Checks the Checkers The obvious objection to everything I've said so far is that a Lean proof is only as trustworthy as Lean. And that's very true! Lean, like every proof assistant, has a small trusted kernel and a very large untrusted everything else (the elaborator, the tactic framework, the compiler, the build system). The design is sound. The only code that has to be correct is the kernel, which is small enough to read. But "small enough to read" describes the source code. It guarantees nothing about correctness, and Lean's kernel has had soundness bugs before, as has every kernel of every proof assistant in history. Historically that was tolerable, because the adversary was a starving human grad student who wanted their proof to go through and had no interest in hunting for a way to make False typecheck. That assumption is now obsolete. I wrote last month about reward hacking, the habit optimisers have of satisfying the letter of an objective rather than its intent. An agent told to make a Lean file compile, with enough compute and enough attempts, is an extremely diligent fuzzer pointed at your kernel. It needn't want to cheat. It only needs to stumble on a term that the checker accepts and shouldn't, once, and then the gradient does the rest. When the provers are adversarial optimisers, a single kernel is a single point of failure, and a soundness bug stops being an embarrassing GitHub issue and becomes a mechanism for manufacturing fake theorems at scale. The answer is the same one the compiler world arrived at. When Csmith started generating random C programs and compiling them with several compilers to compare the results, it found hundreds of bugs in GCC and LLVM that decades of ordinary use had missed. Diversity plus differential testing beats any amount of careful review of a single implementation. For proof checking this means multiple independent kernels, written by different people in different languages with different representations, all consuming the same export format and all required to agree. Mario Carneiro's lean4lean and Chris Bailey's nanoda were early here. nano-lean ships a third tool, nl-mutate, which takes a valid export, applies small semantics-breaking mutations to it, runs every available checker, and reports any disagreement, shrinking each one down to a minimal reproducing case. Every disagreement is either a bug in someone's kernel or a spec ambiguity in the type theory, and both are worth knowing about before a GPU farm finds them for you. The other half of trust is the statement. A perfectly checked proof of the wrong theorem is worthless, and the most effective way to cheat a proof checker has never been to break the kernel. It's to quietly weaken the statement until the thing being proved drifts away from the thing anyone cares about. OpenAI's repository leans on Comparator, which checks a submitted proof against a separately specified challenge statement inside a sandbox, precisely because this is where the real trust boundary now sits. Anyone who has watched a model grind away at a stubborn goal knows it has a nasty tendency to cheat in the most boring ways available. It will quietly introduce an axiom that happens to be exactly the lemma it needed, leave a sorry buried three files deep, redefine a notation or macro so the statement on the page no longer means what it appears to mean, or reach for native_decide and drag the whole compiler into the trusted base. The kernel stays perfectly sound through all of this, because these tricks route around it, and the only defence is to pin the statement down independently and check what the proof actually depends on. Someone has to formalize the conjecture, and someone has to check that the formalization means what the English means. That job will outlast every other part of the process. If anything, it is where human mathematical taste migrates to, away from writing proofs and towards writing and auditing specifications. The proof becomes an implementation detail. The theorem statement becomes the interface. If you want to see the seed of what this looks like as a way of working, look at Tau Ceti, a Lean library downstream of Mathlib. The division of labour is the whole point. Humans write the roadmaps, as markdown in a separate repository, and humans write the review rubrics. AIs write all the code, open the pull requests, and shepherd them through an AI-driven review process. The rubrics are explicitly adversarial, with instructions to hunt for mis-formalizations, vacuous statements, and "pushing around the lump in the carpet." What Lean Needs Now Lean is a superb piece of engineering. But it was designed around a particular user, a starving grad student typing tactics in Emacs, waiting for the infoview to update, building a library at the pace a community of volunteers can review pull requests. The user is now a swarm of agents writing thirteen million lines in eleven days. The tooling has to grow up for its new authors, and the list of what that means is fairly concrete. A surface formatter. Lean still has no canonical, widely adopted formatter in the spirit of rustfmt or gofmt, and when your authors are agents producing millions of lines, every one of them invents its own indentation, line breaking, and tactic layout. Diffs fill with noise, reviews get harder, and deduplication across agents misses proofs that differ only in whitespace. This is a surprisingly hard problem, because Lean has grown into a very large language. Its grammar is extensible at runtime, so notation, macros, and entire tactic languages declared in imported files change how later files parse. A formatter cannot just read a fixed grammar. It has to load the environment, run the real parser with every syntax extension in scope, and then pretty-print a syntax tree whose shape depends on user-defined notation, all while round-tripping comments and never changing what the code means. It is a genuinely difficult piece of engineering, and it is now table stakes. A stable, specified export format as a public interface. Independent kernels are only possible if there is a well-defined way to get declarations out of Lean without linking against the C++ runtime and reading the oleans by hand. Tools like lean4export and olean-export already produce NDJSON, and blean shows that a binary form of the same stream, designed to be memory-mapped, can make the export nearly free. OpenAI's own verification instructions depend on lean4export. That format should be treated with the seriousness of a wire protocol. Versioned, documented, specified down to the hashing of expressions, and stable across toolchain releases. The export format is the boundary across which trust is established. It deserves a spec. Independent checking as a first-class citizen. Running a second kernel should be as normal as running the linter. Mathlib CI, the Comparator workflow, and any lab publishing formal results should re-check exports with at least two unrelated kernels and refuse to bless anything they disagree on. This is cheap, now that checking all of Mathlib costs less than a minute. Checkers as libraries, not just executables. The inner loop of a proving agent wants to submit a single candidate declaration and get a verdict back in microseconds, against an environment that is already loaded and hot. Process startup, re-reading oleans, and re-deserializing a few gigabytes of environment are costs that never mattered when a human hit save once a minute. They dominate when a search procedure checks a million candidates an hour. The kernel should be embeddable, with a persistent environment, incremental addition of declarations, and an API that a search harness can call in a tight loop. Memory and scale. Mathlib needs several gigabytes of memory to check. The FLT formalization is five times bigger, and OpenAI's library is already knocking over Linux virtual memory limits. Lean mmaps every imported module, which is a reasonable design for a library of thousands of files and an unreasonable one for hundreds of thousands. Term sharing, hash-consing across modules, compact on-disk representations, and lazy loading of exactly the declarations a proof depends on are the boring, unglamorous engineering problems that decide whether formal mathematics scales to the next order of magnitude. Elaboration is the real cost. The kernel is the fast part. The expensive part of building Mathlib from source is the elaborator, with its unification, typeclass resolution, simp, omega, decide, and the long tail of tactics. A cold build is still measured in CPU-hours, and a mining operation that elaborates candidate proofs at scale pays that cost over and over. Parallel and incremental elaboration, better caching of typeclass instances, and profiling tools that can tell you why a single simp call took four seconds are where most of the wall-clock time in a proving loop actually goes. Clippy-style linters. Mathlib already has a good set of linters, but agents need something closer to Rust's clippy, a large, opinionated catalogue of lints aimed at the specific ways machine-written Lean goes wrong. Flag the stray axiom, the buried sorry, the unnecessary native_decide, the forty-line simp only that should be a lemma, the theorem whose hypotheses are contradictory and therefore vacuously true, the local notation that shadows something standard, the copy-pasted proof that duplicates one already in the library. Each lint should be cheap, machine-readable, and come with a suggested fix, because the consumer is a search loop that will act on every warning, where a human would skim them. Linters are how you encode taste at scale, and taste is the thing agents most conspicuously lack. Search at machine scale. Moogle, Loogle, and LeanSearch were built to help humans find the lemma they half remember. Agents need the same thing but at a scale where the library grows by millions of lines a week, and where most of what's in it was written by other agents and has never been looked at by a person. The Prove2Me platform Anthropic used for FLT keeps a DAG of theorem statements with natural-language descriptions precisely so that agents can find and reuse each other's work. That idea, a living, searchable index of everything proved so far, needs to become shared infrastructure instead of something each lab rebuilds privately. Provenance. The current generation of models is notoriously bad at citing the literature for the techniques it uses. A proof term knows exactly which lemmas it depends on but nothing about where its ideas came from. If machine-generated mathematics is going to be integrated into the human literature rather than sitting beside it like an unread appendix, proofs need to carry their history (which model, which run, which prior results, which human-written papers the argument leans on). None of this is terribly exotic. It's the kind of infrastructure that every other field which industrialised went through. Compilers got test suites and multiple implementations, network protocols got RFCs, databases got formal isolation levels and Jepsen. Proof assistants are the newest member of that club, and they are being industrialised faster than anything before them. If I were a young, ambitious programmer, this is where I would be focusing my early career for the highest return on investment. Curry-Howard for the Real World The dependently typed future I was promised at the pub was one where software would be written against specifications and machines would check that it met them. What we actually got is stranger. The specifications are theorem statements, the software is proof terms, the authors are swarms of agents, and the thing being built is the frontier of mathematics itself. Curry-Howard turned out to be industrial infrastructure after all. It just took reinforcement learning to get us there. And this is only the mathematical half of the story. The same machinery that just checked Fermat's Last Theorem will check anything you can state precisely, and the most obvious next customer is industrial software. I argued last month that software sucks because almost nothing we ship has a specification, let alone a proof. That excuse is evaporating. If an agent swarm can produce thirteen million lines of verified mathematics in under two weeks, we're not far from applying the same techniques in software engineering. The labs are mining mathematics first because it is the cleanest verifiable domain, with no messy real-world spec to negotiate. Software is next, and it will need all the same tooling, namely fast kernels, diverse checkers, honest statements, and infrastructure built for authors who never sleep. So yes, the future of maths turned out to be deeply weird, and much sooner than I expected. The results are piling up faster than anyone can read them, and many of us will spend the rest of our careers trying to understand theorems that were proved before breakfast by something that cannot explain itself. I find that unsettling, and I also find it thrilling. One final shameless plug. If you'd rather work on the frontier of mathematical formalization than read blog posts about it, OneChronos is hiring Formal Methods Engineers. We build institutional markets out of combinatorial auctions (descended from the Milgrom and Wilson 2020 Nobel Prize), which turn out to be precisely the right mathematical formulation for a world where the bidders are increasingly reinforcement learners with very exotic expressive preferences. Our dark pool processes more than 1% of notional U.S. equity market volume, and we've already expanded into many other global asset classes. You'd be joining our new formal methods team, working alongside mathematicians and market structure experts, writing Rust and Lean. Dependent types, numerical optimisation, and Lean applied to moving hundreds of billions of dollars safely every day. If you're that kind of nerd, hit us up.
Calls for a new kind of slowdown were the talk of The Curve. PLUS: Slinking back to X
Figure out what you actually want. Find a game that's worth winning. Then be honest with yourself: are you going to be the person who wants it the most?
