Do you (or any commenter I haven't read) account for project management gains from claude? I'm imagining that aggregating, summarizing, and ranking bug reports internally at openai and anthropic are worlds different these days than what most PMs and QA departments have historically been like. I think to estimate the "90%" figure properly, these considerations should be a part. Though that may be more holistic than the literal words Dario used in his prediction.
Part of the implementation choices might be alienating-- the day after I signed I saw in the announcement email yesterday "Let's take our future back from Big Tech." and maybe a lot of people, who work at large tech companies, who are on the fence don't like that brand of populism.
epistemic status: jotting down casually to make sure I have a specific "I Told You So" hyperlink in a year or so
I think 9-10 figures have gone into math automation in 2025, across VC, philanthropy, and a percentage of frontier company expenditure (though if we want to look at the latter, a proper fermstimate would I think get much wider than if you were just counting up all the VC bucks). In the startup case, it looks an awful lot like creating press releases to attract funding and talent, with not a lot of product clarity.
I have been guilty in the past of saying "something something curryhoward" is a good reason to be bullish on these startups pivoting to successful program synthesis companies, but in reality I think there are different versions of this belief, and without nuance we start to blend the "strategic landscape of formal methods in AI security" with "ways to persuade VCs to fund you". What I have often meant by evoking curryhoward to justify watching the math automation space for AI safety reasons is that the specific capability of shipping lean proofs disproportionately increases SWE capability, reasoning about programs, etc (this goes 10x so if we end up in the "lean is the successor to haskell" future where companies start shipping lean code to production)[1]. Curryhoward, which is a formal-adjacent correspondence between mathematics and algorithms, is actually stronger than that. It really just means that specs/intent are expressible in a specific logic and that the proofs are executable. But in a hoare logic case, which is how we formally verify imperative programs, and influences most schemes I've heard of for verifying effectful programs, the proof is not the executable!
In 2026, these math companies will start to make their product plays, and I think we'll learn a lot about cognition as we test the hypothesis "how generalizable/economically valuable is pure math ability". However, I think program synthesis companies that do not pursue pure math as a warmup / fundraising strat will take a substantial lead. (this is the core claim of the post that I'm not going to fully justify in this brief memo, just that I wanted it written down in case I can get bayes points from it later). And I roughly agree with Morph's thesis that an outrageously high quality binary grader (i.e. Lean4) leads to RL gains leads to capability edge such that formal program synthesis companies should outperform other program synthesis companies.
and while a wildly successful program synthesis product is dual use, it would enable a lot of infrastructure hardening so has a good shot at providing a great deal of defensive upside. More posts coming out soon. ↩︎
I think there are two categories of traits, the fungible and the nonfungible.
Fungible traits are money, height, BMI/weightlifting. Them being able to pull you is a proxy for their social status.
Nonfungible traits are your actual contributions, what type of person you are, what role you play in a friend group or room, etc. Includes kindness, humor, emotional intuitions, etc.
When girls realize that my nonfungible traits aren't quite their cup of tea, they say "well at least i scored 5'9" / 6 figures / can pick me up and carry me a dozen feet" and then dump me for someone who's 5'10" / 7 figures / can pick her up and carry her two dozen feet. But if my nonfungible traits are her cup of tea, fungible traits don't seem to do much of anything!
In other words, fungible traits are the fallback when a girl doesn't like you very much. They're literally only worth considering if you assume she doesn't like you as a premise.
I think the answer is that clothing is halfway between, or plays both roles. Clothing contributes a lot to the "my friends will think I pulled well if I bring you around them" factor, so they're like a fungible trait. But clothing is also a vector of self expression, and to many it's a conscientiousness proxy / proxy to how clean your room is which people are screening for in long term primary relationships.
So idk.
forgive me for not finding the specific citation, but I believe I first learned about this in a Kevin Carson essay on "diseconomies of scale" and systemic inefficiencies of large organizations many years ago--- yes-man psychosis played one role among many.
there's an analogy between the zurich r/changemyview curse of evals and the metr/epoch curse of evals. You do this dubiously ethical (according to more US-pilled IRBs or according to more paranoid/pure AI safety advocates) measuring/elicitation project because you might think the world deserves to know. But you had to do dubiously ethical experimentation on unconsenting reddizens / help labs improve capabilities in order to get there--- but the catch is, you only come out net positive if the world chooses to act on this information
I don't know what legible/transferable evidence would be. I've audited a lot of courses at a lot of different universities. Anecdote, sorry.
One thing I like about this is making the actual difficulty deltas between colleges more felt/legible/concrete (by anyone who takes the exams). What I might do in your system at my IQ level (which is pretty high outside of EA but pretty mediocre inside EA) is knock out a degree at an easy university to get warmed up then study for years for a degree at a hard school[1].
In real life, I can download or audit courses from whatever university I want, but I don't know what the grading curve is, so when 5/6 exercises are too hard I don't know if that's because I'm dumb or if 1/6 is B+ level performance. This is a way that the current system underserves a credential-indifferent autodidact. It's really hard to know how difficult a course is supposed to be when you're isolated from the local conditions that make up the grading curve!
Another thing I like about your system is tutoring markets separated from assessment companies. Why is it that we bundle gatekeeping/assessment with preparation? Unbundling might help maintain objective standards, get rid of problems that look like "the professor feels too much affection for the student to fail them".
This is all completely separate for why your proposal is a hard social problem / a complete nonstarter, which is that I don't think the system is "broken" right now. There's an idea you might pick up if you read the smarter leftists, which is that credentialism especially at elite levels preserves privilege and status as a first class use case. This is not completely false today, not least because the further you go back in time in western universities the truer it is.
my prior, 15 years ago, looked like "stanford has a boating scholarship, so obviously selectivity is a wealth/status thing and not reflective of scholarship or rigor", so the fact that I now believe "more selective colleges have harder coursework" means I've seen a lot of evidence. It pains me, believe me, but reality doesn't care :) ↩︎
Social graph density leads to millions of acquaintances and few close friends, because you don’t need to treasure each other