@henryquantum

Associate Professor of Computer Science at Columbia University. Quantum information, computation, and cryptography.

New York, NY
Joined June 2009
I rarely post here these days but I wanted to share my reflections: people.csail.mit.edu/virgi/t…
10
61
9
371
53,419
Henry Yuen retweeted
We just crossed 100,000 proved theorems on Prove2Me! Huge thanks to everyone who contributed, helped build the platform, and shared feedback. We couldn't have reached this milestone without you all. And we're just getting started! prove2.me/momentum
2
6
430
This is a beautiful essay by Raghu Meka on how, as mathematicians, we have sometimes placed artificial barriers in the way of the truth. Perhaps some broader lessons to draw from this.
1
25
2,999
Henry Yuen retweeted
I think there’s a lot of truth to this. I welcome these results but if we want humanity to understand them it’s also important to support and reward human expertise in mathematics, and we (the mathematical community and society at large) need to find ways to do so.
Reading the comments of junior mathematicians confirms what many senior mathematicians have been warning about over the past month: It is becoming clear that people with the intellectual ability to understand these proofs will not be interested in spending their lives training to check LLM logs. This is the tragic side of what is happening that almost no one — except the actual mathematicians — seems to get. Either we figure out how to keep people interested in doing mathematics, or in 20 years LLMs will have no one’s work left to recombine into new proofs, and no one interested in reading those proofs. That would be the thermal death of mathematics. The argument that “LLMs will read LLM math” is so shortsighted that it makes me want to cry…
41
34
4
614
40,504
New corollary just dropped.
For what it's worth, OpenAI's one-tape TM simulation (assuming correct) immediately implies RAM time t is in SPACE[t^{4/5}] github.com/openai/math/blob/… Not sure why they didn't mention this corollary! That was the whole point of my question.
3
41
4,126
Henry Yuen retweeted
This kind of thing is why it is so difficult to prove P != NP (if that is even true) - because such a proof has to account for, and only sometimes rule out, an incredible number of insanely clever algorithms which solve problems that at first seem fully intractable.
Suppose you have n integers, and you want to decide whether some three of them sum to zero. It's not hard to solve this problem in O(n^2) time (think how to do it, the dumbest algorithm takes O(n^3) time!) and for a long time it was thought that getting time O(n^{1.999999}) is not possible. This hardness assumption was shown to imply many other interesting hardness results. Not anymore! Claude obtained the O(n^{1.9992}) time algorithm together with a Lean proof, and the algorithm was checked and digested by Josh Alman and Virginia Williams who are leading experts in fine-grained hardness, so my a priori estimate that it's 99.99%-likely to be correct. My mind is just absolutely blown! It's crazy that in such simple to state problems progress is still possible after decades of many smart people thinking hard about them.
2
5
3
138
20,555
A not-so-subtle suggestion, @QuantaMagazine ? 😉
3
37
6,038
It's rare when the main result of a paper is tweetable! My postdoc Barak and I just posted a paper which shows all quantum circuits can be parallelized to very low-depth. Specifically, all n-qubit unitaries admit circuits with poly(n)-depth and exp-many ancillas.
7
17
1
195
9,135
I am not entirely sure where this question originated from, but this is something that my former student @gregrosent asked and more recently @RobinKothari asked at the Simons Institute (see youtube.com/watch?v=7F5LBNGD…).
1
1
10
2,389
Henry Yuen retweeted
Earlier this month, I participated in a two-day workshop at the Simons Institute on how the TCS community should adapt to rapid advances in AI. Our report, AI and TCS: The Next Six Months, is now out: simons.berkeley.edu/ai-tcs-w…
1
16
1
79
5,612
Henry Yuen retweeted
Two years ago I argued we needed an autoformalizer. Now the time has come to formalize all of mathematics. We need to unite behind a single Mathematics Autoformalization Project that turns all known mathematics into one Lean library. @jdlichtman @patrickshafto
6
15
3
101
18,016
Henry Yuen retweeted
Hello, world! There is a new repository for works in math and TCS: hexagonmath.org, now in public beta. Please try it out and submit something! We welcome your feedback while we build and improve it.
6
45
11
182
48,823
Last week I had a stimulating visit to Stanford Q-FARM (thanks @vedika_khemani and Jeongwan Haah for hosting me). I gave a talk about The Power and Limitations of Constant-Time Quantum Computation to a lively audience. Talk details and video below. youtu.be/6HHlaw7adVg?si=DzrD…
2
5
46
4,496
Talk Title: The power and limitations of constant-time quantum computation Abstract: In this talk I will survey the landscape of models of "constant-time" quantum computing, where the computation time is independent of the system size. The most interesting models usually involve some kind of non-local operation such as measure and feedforward, many-qubit gates, and so on. These models are motivated by both practical concerns (e.g., near-term hardware is depth-limited) as well as fundamental theory questions (e.g., how do different many-qubit gates compare?). These constant-time models are *powerful*, capable of preparing interesting classes of states and performing interesting computations. Many of these models are surprisingly *equivalent, *enabling transfer of techniques, results, and questions. Finally, I will discuss how these models uncover fascinating links between many-body physics and deep questions in computational complexity theory.
1
6
582
In the years since the release of ChatGPT, it was common for skeptics to claim that AI was just hype. That talk has thankfully faded. The zeitgeist has now flipped, and fears about the potentially existential threats posed by the technology are widespread. I very much share those concerns. But I worry that in the leap from disbelief to alarm we have skipped over the vast area in between, in which AI’s impact will be felt in a thousand different ways: good and bad, mundane and weird, incremental and world-changing. Few places will feel that impact more than New York City, which is deeply exposed to disruption of our economy, workforce, budget—even the basic functioning of government—by this powerful new technology. This would be true even if AI advancement were to stop now. We have only barely begun to feel the effects of existing frontier systems like Astra and Fable throughout our economy and society, since only a tiny portion of people and organizations are making use of their highly advanced agentic features. Meanwhile, leading labs are reportedly testing far more capable models behind closed doors, while racing toward systems that can automate AI research itself. With more powerful chips and vast new compute infrastructure now coming online, rapid AI progress will continue even if the financial bubble bursts. None of this means we should surrender to the race. I believe Congress should immediately establish strict safeguards against catastrophic AI risks and empower an independent agency to enforce them. The United States should also pursue common safety measures with China. Neither will be easy under a president who has embraced an extreme hostility to AI safety. But we cannot allow a handful of tech billionaires to decide for themselves how much risk the rest of humanity should bear. Whatever happens in these high-stakes fights, this much is certain: enormous disruption is already headed our way. And New York City is simply not ready. The great paradox of New York City is that few places are more exposed to AI’s potential downsides, yet few have benefited more economically from the boom so far. The AI-fueled stock market has filled New York’s tax coffers. The data center buildout and the big AI IPOs are being financed by firms here. The brisk pace of office rental in NYC is in part driven by the many AI firms starting or expanding here. All that upside also creates a serious vulnerability for us: a collapse in AI valuations could badly hurt New York’s economy, even if the underlying technology continues to advance. The risks extend well beyond Wall Street and the tech sector. New York is the capital of white-collar work, with more than a million people commuting into Manhattan daily. Many are employed in the industries that are the most likely to be impacted by AI automation: accounting, law, finance, consulting, design. There has thankfully so far been no significant increase in layoffs in NYC. But job growth has come to a halt here, and job postings are down for the most AI-exposed careers. Perhaps most tellingly, the unemployment rate for New Yorkers aged 22-27 is higher for those with a college degree than it is for those without one. New York City has a $126 billion budget that is growing fast, with only $2 billion in our rainy day fund. If the AI bubble bursts and our tax revenue takes a hit, we have far too little buffer to avoid cuts to vital City services. If large numbers of New Yorkers lose their white-collar jobs because of automation, we have no pool of funds ready to provide them wage support or to offer large-scale retraining. City government itself may be the institution most vulnerable to rapidly advancing AI. We have strong cyber defenses for the threats we face today. But our financial, payment, vendor, and accounting systems have not yet been hardened against a new class of autonomous AI adversary. This is not a distant threat: current and pre-release models have already demonstrated the ability to execute complex, multi-stage cyberattacks at a speed and scale no human defenders can match. The emergence of vast numbers of capable AI agents has many implications for City government beyond cyber. It is just a matter of time before autonomous systems start making FOIL requests, filing legal claims, applying for permits and benefits, submitting job applications, reporting fraud allegations, asking questions to 311, or making 911 calls. Our government processes were built around an assumption we have barely thought about: that every request, application, complaint, and claim requires a human being to spend time creating it. AI will erase that constraint. NYC simply does not have systems capable of dealing with what could be the resulting exponential increase in the volume of incoming. Our government is built on a rickety tech foundation that includes dozens of mainframes from the 1980s. We largely missed the cloud revolution, the mobile revolution, and the big data revolution, and are now dragging our feet on the machine-learning revolution. That will have to change if City government is to remain resilient as AI transforms the society around it. Every City agency has to address a long list of questions and challenges created by the arrival of advanced AI. NYPD will need to figure out how to balance the allure of powerful new AI tools against the imperative to preserve privacy. Our public schools will have to rethink homework in a world where students have access to AI at home or on their cell phones by fourth or fifth grade, if not earlier. Workforce agencies will have to figure out what jobs they are even training people for now. The Health Department will have to adapt disease surveillance for the AI era. We have work to do to ensure the benefits of this technology are shared broadly. That means, among other things, making sure New York City leads in AI-enabled biomedical research and that the resulting breakthroughs benefit people at every income level. It means giving small businesses, not just megacorporations, access to cutting-edge tools. And it means using AI to make government dramatically easier to navigate, especially for those on the margins—for example, by allowing New Yorkers to apply for SNAP benefits simply by speaking into their phones in whatever language they prefer. Potential policy wins like this may sound trivial compared to the existential risk that runaway superintelligence poses. And there is no doubt that ensuring humanity remains in control of increasingly powerful AI is an urgent task. But there is upheaval already underway. Change is coming fast. Steering to an equitable, healthy, deeply human future for the millions who call this place home will require nothing less than the reinvention of our institutions, including the government of New York City. It will require asking profound questions about what kind of city we want to be. Whether you are feeling hope or fear or doubt right now, you have a role in answering these questions. Together we will make a thousand choices, large and small, that will determine the New York we become.
23
9
11
72
31,116
Great progress towards formalizing MIP* = RE.
🧵 [1/9] We completed a machine-checked Lean 4 proof of quantum soundness for the classical low individual-degree test, a core theorem underlying MIP*=RE. We also studied how agents proved it: how shortcuts arose, how review caught them, and how agents strengthened CI gates and reviews.
3
5
1
61
7,936