Full Width 
Shortcuts 
Sign Up 
Log In 
Articles 
Reading List More from Aaron's Essays
Jews do mourning well. That’s what I’ve always thought from watching family and friends go through it. It’s what I’ve learned as fact since my father died eleven months ago. There’s a central tension to it. A constant fault line that our customs straddle. It’s the constant struggle of an individual and a member of community. To be sure that’s one of the central themes of Judaism itself. We take responsibility for the commandments ourselves - each of one of us. But we do so many of them as a community. A person keeps kosher, shabbos, honors his parents. The community prays, builds, comforts and protects. I and Thou, sort of. 1 I found this pattern in the second after my father died. This isn’t where I get specific. But those moments are the loneliest in the world. Even with my mother and my siblings there. These moments are lonely not simply because they are but because our laws tell us that, at that moment, we are forbidden from completing the time bound laws of Judaism. These are ones that are so often tied to community. We cannot eat meals with friends and bless our food. We do not pray with a minyan. There is only one thing, to prepare for the funeral - really the burial itself. And so I sat alone - with other people, with my wife - but alone with my thoughts of my father. I chose to write a eulogy, though not everyone does. You are alone. But not for very long. In fact our laws say that you must do everything you can to bury the deceased before the next nightfall. You must do it with others. For a variety of reasons. The one that gives the most strength is that a burial means saying kadish means getting a minyan together to respond. At the least. I recently listened to a Jew who was raised in the USSR say that the only communal Judaism she knew as a child was when 11 men would gather secretly to say kaddish. 10 to make the minyan. 1 to watch out for the KGB. I was lucky in this. We had more than a minyan. We had a synagogue full to bursting with people who loved my father, or me, or my siblings or mother or who loved people who loved my father. He was easy to love. So I crossed - alone to community. Though you can be alone even surrounded by people. The first kaddish is lonely. At the graveside. But I could hear my brother and sisters and mother and the rabbi. I was lucky. It felt a little less lonely. 7 And then we come to Shiva, the “Seven”. Maybe the greatest thing we do though you only learn that when you are forced to do it. Our tradition does not allow you to be alone during the time that you want to be alone more than anything. It started after burial. That evening with a minyan at our house. I led services. Haltingly uncomfortably stumbling through words I mostly knew but hadn’t paid enough attention to in years. Though even there, the tension is constant. I was with other people, but I was also alone. Even saying the kaddish out loud requires you to chant words in dead language - aramaic - loud enough that others can hear you and respond. The constant thought is “what if I mess up.” The answer is that no one will notice and if they do they will give you comfort and gentle help. And you’ll do it. Each day our house filled with people and we told them stories and they told us stories. I’d speak to the room, and feel…not alone. My siblings and mother would speak, and I could feel the warmth of other people. There’s a beautiful and strange thing we say when we leave a house of shiva. “HaMakom yenachem et'chem b'toch shar avay'lay Tzion vee'Yerushalayim.” It effectively means “May God comfort you amongst all the mourners of Zion and Jerusalem.” In this case “you” is plural. Which begs a question: what if you are sitting shiva by yourself? Our rabbi explained - even when a mourner is alone, the spirit of the deceased is by his side. God is by his side. We’re never alone even when we want to be. There is always comfort. 30 After the shiva comes the strangest period of mourning, the Shloshim or “Thirty.” This liminal period contains many of the restrictions of shiva - no haircuts or shaves, no new clothes, limited interactions with groups, no parties. For me, the hardest part of it was going to minyan daily. Going three times per day. Leading nearly every service I attended which is meant as an honor but comes with the designation of being a “chiyuv” or a “requirement.” How strange it is to be in a room with people I often did not know and being told to get up in front of everyone, by myself, and lead services. How lonely. But, the response to the kaddish. The same everywhere every time. With warmth and feeling. The questions in each new place I went “Who did you lose? I’m so sorry, do you want to tell me about him?” What a forcing function we have to connect to our community to tradition to what we’d lost. Then one day shloshim ends. 11 The final period of active morning does not have a name I know. What I do know is that for the last 11 months I’ve done my best to go to minyan every day and say kaddish for my father. Usually I made it three times. One time I missed them all. I was lucky and I was determined. 11 months for various reasons though the one in my head is that all souls go to something like purgatory. We say kaddish to aid their progress to the world to come. Only the most evil of humans stay longer than 11. So we stop before the natural 12 months. My life rotated around finding places to go. Synagogues and offices and houses and one time a cafeteria that was empty. Each time it was a reminder to think of my dad. Each time I raised my hand to say “I’m chiyuv” I felt the fear of standing out, of being alone, of identifying myself. Of remembering that I was sad. Each time I did I was met with warmth and understanding. The ends of things sneak up on you. We thought - my siblings and I - that we’d finish kaddish this weekend. My brother did more research and found out that today is somehow the end. It echoes death. Sudden, unexpected. Less climactic than personally cataclysmic. A sundering and rupture and a quiet fall into the unknown. I’ll say kaddish as a mourner for my father for the last time this afternoon. The emotions are wildly complicated in ways I didn’t expect. Sad to lose this anchor, happy to be free of the requirement, curious what I’ll do with the flexibility. Mostly I miss my dad. But losing him bound me more tightly to the community I was born to and to the ones I’ve chosen and made. This is what our mourning does. It forces the individual to look within and then rebind himself to the many. It forces the many to look at the mourner and offer support and kinship and comfort and place. 12 The final moment of religious mourning will come in a month. It will come with its own struggles, its own moments. We know what to do with it, we have customs for it, for the yahrzeit, the anniversary. But that’s for later.
I’ll be addressing the topic below along with Alfred Lin from Sequoia and Ilya Sukhar from Matrix on 3/24: https://us06web.zoom.us/webinar/register/WN_qgghYDq4QxCiW9REOOrbmw It would be challenging to name all the fundraising mistakes that founders make during the many demo days that occur each year. There are certainly broad categories, but rather than focus on all of them, I think it’s worthwhile to consider one specific category of error, which is generally one of omission rather than commission: ignoring demo day as a step toward an A. This is a big one because, at least when I ran the data at YC, the best companies in an accelerator tend to be the ones that raise a Series A within 12-18 months of Demo Day (or sometimes a month or two before Demo Day). There’s a strong correlation here driven by the fact that the best companies tend to set and maintain a rapid pace of growth throughout their lives, and that trend leads to rapid milestones. And yet, most founders I talk to treat their Demo Day as a disconnected event. It’s worth thinking about why they do this, what behavior it causes, and how to correct it. On the why: I think it’s fairly simple. Demo Days are stressful and are built and run around the idea that the sole purpose is to raise seed funding. This is true but also misses the point because seed funding isn’t the goal of a company - building a big company is the goal of a company. From that lens, Demo Day and seed funding are part of a larger story, and are tools for executing on a larger vision. Now, many founders will say that they don’t have time to think about their A when putting together a seed, but that’s short sighted. Founders should be thinking about every round they do as it relates to the next round and the next set of milestones the business needs to achieve. You can add to this that most of the advice founders get from various advisors around Demo Day is to close money fast and go “back to work.” But again, this is short sighted. A Demo Day is the only time where many investors are hyper focused on an early stage startup. Squandering that attention is a mistake.[1] Of course founders shouldn’t constantly be actively fundraising, but they sure as hell need to always be thinking about where the money they need to build is going to come from. On top of that, they need to act in a way that increases their chances of raising that money. One more thing - last time I ran the data, it turned out that having a Series A investor in your seed was, on balance, a positive signal for your ability to raise a quality A. I’m sure the numbers have shifted a bit since then, but I’m willing to bet that the conclusion is the same. So, to get to the errors: Don’t ignore Series A investors before or at a Demo day. If you do not plan on raising an “A,” find a way to schedule time with them anyway. Don’t shoehorn Series A investors into the same process that you have for angel/seed investors. They generally work differently, so account for that. Don’t think of your seed round as an isolated event. Think about the amount you raise and the cap you use as a starting condition for your next raise. Limiting dilution is good, on balance, but not if it gives you a cap so high as to impair your ability to raise your next round. Don’t vanish after meeting an investor who seemed interested and who has a good reputation. Figure out how to nurture that relationship and keep the investor interested. Don’t treat investors as interchangeable. It may be true that money is money, but the people deploying it are human and want to build a relationship. You are not trying to make friends, but you are playing a game that is designed to increase the chances of success for your company. Avoiding these errors isn’t necessary or sufficient to raise an A. I’ve seen companies commit nearly every error imaginable and still raise money. However, founders shouldn’t strive to be uniquely lucky in fundraising. Founders should use knowledge about how fundraising works to constantly improve their odds of success. A demo day is an unfair advantage in that process, and founders should treat it that way. __ [1] This goes for the accelerator as well as for the founder. Accelerators should harness the interest of later stage investors vs. designing fully against their interests.
Let’s accept, for the purposes of this essay, that founders and venture capitalists are engaged in a simple trade. Founders sell business risk for the cash they need to take bigger risks; venture capitalists buy that risk hoping it will one day transmute into reward. Each side does this because they believe that, ultimately, the size of the risk is directly correlated to the scale of the potential reward. But there’s acceptable risk and there’s unacceptable risk. No sane person is going to invest in a scheme to turn lead into gold, but early-stage startups—and even some mid- and late-stage startups—rarely present such a clear-cut profile. Investors are often under pressure to evaluate seemingly great ideas and teams without all of the information they’d ideally have to decide whether to put their money on the line. I’ve written in the past about how investors consider the reward side of this process, so let’s focus on the risk side. Some risks are obvious—the market may be too small or the costs too high—not to mention that pesky fact that the future is always ultimately unknowable. But some risks are more idiosyncratic. We call these red flags. There’s been a lot of talk about red flags recently, mostly in the context of FTX and the diligence that its investors may or may not have done before committing their partners’ funds. I happen to believe that investors did a heck of a lot more diligence than they’re being given credit for having done, but I also think that conversation misses the point. Red flags, when you find them, are rarely deal-killers. They’re just pieces of information, indications of risk. The bigger the reward potential, the more red flags an investor should be willing to accept—or even expect. Let’s take a look at a specific type of red flag I’ve seen and the nuances it presents: During the diligence process, an investor discovers that the numbers in a pitch don’t match the numbers on a revenue or income statement. This is, without a doubt, cause for concern. There are two major explanations here—either the founder made a mistake or the founder is lying. If the founder doesn’t seem to understand the numbers, the investor will probably decline the deal—not because of any specter of dishonesty, but rather because the founder is demonstrably incompetent. If the founder gets evasive when confronted, the investor would probably conclude that they’re lying and walk away. But if the founder recognizes the discrepancy as a mistake and quickly corrects it, provided the error is fairly trivial, the investor may lose some confidence but not give up on the deal. There are other classes of red flags. Sometimes the corporate structure is odd (this was true of Facebook, which in its earliest days granted founder Mark Zuckerberg enough super voting shares to ensure his will would go virtually unchallenged), or the company was originally a non-profit (see: OpenAI). Founders get flagged for not thinking deeply enough about a problem and for thinking too deeply about a problem without taking action. Some investors believe that being a first-time founder is a red flag in and of itself, while others see it as a strong positive. Remember: Red flags are very rarely outright fraud, and when they are, it’s often obvious only in hindsight. Different investors have different levels of risk tolerance and generally only agree with each other when someone else makes a catastrophically bad and public mistake. Especially in a later stage company, there are so many places for a malicious actor to hide their dirty dealings that it would be incapacitating for any investor to do all the diligence required to definitively eliminate fraud. Such a thing simply isn’t possible. Look at Enron! Look at Madoff! And finally, on the other side of any red flag is one critical, inescapable question: If the product is selling and the company is making money, how big a problem could it be? What if what looks like a red flag turns out to be a meaningless distraction and the deal you walked away from nets someone else a billion-dollar return? I’m willing to bet that there are investors who passed on Google’s Series A in 1999 because it had almost no revenue—a clear red flag for a company raising $25 million—and are still kicking themselves for it. All of which is to say that so-called red flags matter, but not in any kind of mechanistic way. And if you flip that around, there’s an important lesson here for founders. Every business has flaws that could be considered red flags by someone. (If there are absolutely no red flags, that could be the biggest red flag of all! But I digress…) One of the most useful things a founder can do when preparing to raise capital, therefore, is to take as objective a view as possible of their business and know where those red flags are. For instance, delivery businesses generally have low margins relative to software businesses. Some investors won’t touch delivery for that reason, but most are happy to dig deep provided that margins are improving at a high enough rate that they can turn a hefty profit before the company implodes. One of my favorite misunderstood red flags has to do with the default rate of a lending business. Many founders work hard to demonstrate that their default rate is, effectively, zero. This feels smart, like perfect risk-management. But it is also almost always the wrong answer. Lending requires at least some risk, so if the default rate is zero, it means the founder hasn’t stress tested their model on a broad enough range of users. What investors actually want to see is a reasonable default rate within the context of factors like the cost of capital, the ease of scale, the return profile, etc. As long as the default rate makes sense within the overall story of the business—and that the story ends in huge returns—no red flag. The best thing a founder can do is to draw attention to their red flags proactively and in detail. See this unusual management structure we have? That’s on purpose. See this gap in our revenue over here? We screwed up, here’s how and here’s what we learned from it. In the end, what matters is context—the way whatever red flags there may be fit into the larger narrative of the business. No red flags mean no risk at all, and that wouldn’t be particularly interesting. __ I originally published this in by The Information on Jan 18, 2023: https://www.theinformation.com/articles/red-flags-are-in-the-eye-of-the-beholder
Originally published in The Information on November 2. For the past nine months, nearly every investor with a Twitter account, blog or board seat has been beating a unified and constant refrain: The go-go days are done. Founders were being pushed to build 36 months of runway, whether or not it was actually feasible to cut costs that much. Time and again, investors told me due diligence was back. I watched as fundraising rounds that a year ago would have produced a term sheet in a few days stretched across a full month and dozens of pitches. And then came Dall-E 2’s public release, quickly followed by a flood of wildly cool technology. (edit 12/8: And now ChatGPT!) These events triggered a craze now ripping through venture capital land. We’re seeing billion-dollar valuations for companies peddling products based on generative artificial intelligence algorithms with less than a million dollars of revenue and no proven business model. Not long ago, the same behavior was held up as a cautionary tale about the excesses of VC over Web3 and instant delivery. Now we have a whole new era of exuberance on our hands. The first thing to remember is that this ability to pivot from dark depression to fall-over-yourself excitement is at the core of the startup world’s future-building powers. Seen from another angle, the whiplash looks like optimism, and VC would have vanished decades ago without it. The entire venture model is about funding failure until you find success. There have been times where the entire industry seems to implode, only to come roaring back. I won’t argue that every investor or founder is a walking example of this kind of stoic hopefulness. There are plenty of cynics puffing themselves up by tearing down other people’s ideas (something I—regrettably—did quite a bit of early in my career), and plenty of others who have no particular view on the future other than wanting to make money. The best investors and founders, though, are optimistic realists of the purest sort. This might come across as ignorant or naive, but sooner or later they usually end up being right. Optimism is the key to understanding what’s happening on the frothy edge of the investing world. It would be easy to write off the generative AI craze—after all, there was an AI and machine-learning craze just a few years ago that didn’t lead to much of anything. Add to that the ongoing collapse of several waves of exuberance at once—crypto, fast delivery, public markets in general—and it’s difficult to believe that optimism will actually win out. That said, I see four major reasons why generative AI has venture capitalists acting like it’s Q1 2021 all over again. It’s rooted in an archetypal category of futuristic technology, aka AI. There are any number of plausible paths that end in fat returns. The press has already thoroughly hyped the space as a whole and a handful of companies in particular. Most importantly, there are no public generative AI companies. As a result, there are no visibly crashing multiples or valuations to weigh down private valuations. Coming out of the stock market crash at the beginning of the Covid-19 pandemic, the world did in fact change. Work shifted, shopping habits morphed and the value of venture bets hit astronomic highs. Companies that had been private for a decade decided the time was right for blockbuster initial public offerings, and Wall Street said, “Hell, yes.” That meant big payouts for all the venture investors who’d been patiently waiting for their exit opportunities. As returns surged, new fund sizes surged, and the FOMO cycle kicked in all along the chain. Suddenly it was easy to be optimistic—too easy. Wherever there was software, or even just the idea of software, there was the promise of quick wealth. Then many of the equities that went public to great fanfare quickly fell off a cliff, taking a whole lot of optimists with them. By spring this year, pessimism seemed to have set in. On its face, this was more than a bit baffling. It’s not as if much value has been destroyed—sure, the valuation of, say, Coinbase has dropped more than 80% since its public trading debut, but a market cap of $15 billion is still incredible. Plus, as I’ve already argued, investors are sitting on huge piles of money and they have an obligation to invest. What’s become clear in the last month is that the ancient optimism wasn’t dead, it was merely hibernating. Maybe you could have seen this from the ongoing drumbeat of new fund closes. If you’d talked to the right investors, you’d have discovered that they were still doing deals, just quietly. The market was waiting for a catalyst, and now it has one. It’s important when thinking about how VC works over time to remember that venture investing is driven by narrative more than it is by data. Early-stage companies are valued on their promise, not on what they’ve done. On top of that, an awful lot of venture capitalists devoured science fiction as kids and now, as adults, they fixate on how new technologies can shift humanity. Even if we haven’t yet figured out a positronic brain or proton micropile, AI always tickles that old childhood fascination. Generative AI especially offers tantalizing possibilities. If this new stuff can write marketing copy, is it good enough to topple the world’s largest advertising agencies? It’s possible that image generators will soon remove the need for commercial photography. Maybe we will finally get a conversation engine that makes customer service less awful and renders the call center business obsolete. Each of these is a giant opportunity, and we’ve barely scratched the surface. With the narrative pieces in hand, investors have another hurdle to overcome: peer pressure. Some investors seek out genuinely novel bets, but many want the safety of going with the crowd. Generative AI satisfies both desires, having both whiz-bang appeal and enough press attention to give timid investors cover. It’s all good news for venture capitalists and founders in the generative AI world right now. That won’t last, but right now, it’s easy to argue that the future is bright and golden. Even more, it’s difficult to tie these new companies to the types of public assets that have been hammered of late. Generative AI isn’t software as a service, so SaaS multiples are irrelevant. It isn’t a token, so crypto winter doesn’t matter. For the moment, at least, nothing can spoil the party. All of this is great for the tech ecosystem, including for founders not currently building generative AI companies. That’s not to say companies should start adding random image generators or copywriting features to, say, payment processors. That would be foolish, though I’ve seen worse (not every videogame needs non-fungible tokens!). The lesson for founders is that investors are looking for reasons to be optimistic. Sometimes that means cutting back on hiring or reining in growth plans, but the really savvy founders will find ways to convince investors their companies are the ones that can swim against the current. Let’s all hope generative AI fulfills at least a quarter of the promises people are making in its name. In the meantime, optimism is contagious, which is good for everyone.
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?
