Kevin Lacker

I'm happy to announce the launch of Acorn, a new theorem prover that includes an integrated AI. Theorem provers let you write mathematical proofs that are rigorously verified. But they are notoriously difficult to use. Acorn makes it easier, by using AI to fill in the details.

@bscholl I wonder, how hot is the inside of an abandoned jet in Tucson in August

For less money than a studio in SF, you could live in a stored Spirit jet in Tucson.

@tamaybes To be truly autonomous, AI must lead the meeting that decides on the official launch date

I think this claim that there's a ~60% chance of a frontier model 'autonomously training a successor version of itself' by 2028 is misleading. Successor models typically involve scaling up compute and data, which I don't think will be automated, nor does Clark claim it will.

@samth @littmath @blueblimpms That makes sense. Personally, I predict that teaching is the last thing to change. What I hope is that we get more "software engineering for physicists/biologists/economists(/mathematicians?)" classes that embrace the AI-coding future.

@lacker @littmath @blueblimpms I agree that US math _research_ spending is likely <$1B. But research is heavily subsidized by teaching.

This is a characteristically thoughtful and coherent account of mathematics from my colleague Jacob, and I agree with much of what he writes. But I want to push back on some aspects, which don't accord with my experience of or motivation for doing mathematics. Problem-solving I fully agree with Jacob that, as currently practiced, problem-solving is a fundamental aspect of doing mathematics; like Jacob, I identify as a "problem-solver" more than a "theory-builder." (A related axis: I identify more as a "frog" than a "bird.") Why do we solve problems? For some of us, it's more or less about enjoyment. That is NOT why I solve problems. I enjoy parts of that process: getting the solution, some little moments of understanding along the way. But my primary emotional experience of problem-solving is not fun: it's frustration. I try to understand something and get confused and I HATE that feeling, and need to resolve it. For a while my bio on here read "forever confused" -- that's not an exaggeration. I think the main reason I (and many other mathematicians) solve problems is that it's the only way we know how to ground ourselves in mathematical truth. Without solving problems and working out examples, our work inevitably devolves into bullshit. The activity of mathematics So is 80%+ of mathematics about problem-solving? I think this is a coherent account of mathematics but it's not my experience. Like Jacob and many other mathematicians my work is indeed guided by some big problems: for me, the Grothendieck-Katz p-curvature conjecture, some questions about mapping class groups, some questions about fundamental groups of algebraic varieties. Many of these problems have occupied me for a decade+ now. My experience of thinking about these problems is, perhaps paradoxically, not about "problem-solving." Rather, these problems benchmark our failure to understand certain fundamental phenomena: differential equations, surfaces, polynomials. It's useful to have rigorously stated problems like this to guide the field, but I think they have relatively little influence on my day-to-day work. That looks more like: trying to identify the most basic situation in which our understanding fails, and develop it in that basic situation. In this model, problem-solving is secondary: my typical experience is that I think I understand something new, often non-rigorously, and then try to operationalize it to solve some problems both to test the correctness of this understanding, and to measure its effectiveness. It's not uncommon in this model for a problem and its solution to appear at the exact same time. In fact, for me, it's somewhat unusual to write down a rigorous statement of a lemma that I do not already know how to prove, though this does of course happen. Oracles Jacob proposes the a thought experiment, where one has access to an AI oracle that can solve rigorously-stated problems better than humans but has less capability in other areas of the mathematical process. Like him, I do not expect this to be the long-term situation--eventually I expect AI mathematics to exceed humans in every mathematical capability--but let's run with it for a second. What would mathematical activity look like with such an oracle? Jacob writes: "Well, you make a definition, and want to know if it’s the right one. You immediately ask your oracle a thousand questions. From “are these basic properties true” to “ooh, so is this deep conjecture true?” and start getting back answers, and amending your definitions. You could invent and resolve entire research directions in days. But the confusion you would have had to push through to flesh out your theory would largely (probably not entirely) be instantly resolved and the whole process sped up tremendously by your oracle. A big part of the process would be gone." I think this is where I most strongly disagree with what he writes. I think you start getting back answers, and then to continue, you have to UNDERSTAND them. And the dirty little secret of mathematics is that it's impossible to understand what anyone else is saying. Conveying one's mathematical intuition is incredibly hard: at least for me, the experience of acquiring understanding from someone else's work is nearly identical to that of discovering it on my own. Of course, what the mathematics of the future will look like depends (like all AI prognostication) on the precise shape of future AI capabilities; I do not think the picture of an uncreative oracle is realistic. I expect future AI mathematicians to be creative, and also, not to be oracles. I think a lot of the questions we view as fundamental will remain open for some time. Basic mathematical questions can be arbitrarily hard! And we will still want to understand them. Doing math Most of what I love about the practice of mathematics is: talking to colleagues about math, learning and understanding new things, developing intuition and resolving confusion, etc. My sense is that these parts of math survive with arbitrarily capable AI tools. I also like a lot of other aspects of the job: I get paid and can afford to eat, I have a lot of intellectual freedom, I have great colleagues (like Jacob), I don't have a boss and can work sprawled out on a couch. Absent a real attempt for the profession to adapt to the coming changes, it's possible that the shape of the profession changes in a way that makes it much less enjoyable, even as most of what I like about doing math survives. There are questions as to why society should support human mathematicians if and when machines have absolute advantage over us in all aspects of mathematics. I think we'll have advantage in some aspects of mathematics for some time, but it's worth thinking about this endpoing for the profession, as it is for all other professions. That said, I think there's a future here where we continue to ask basic questions about fundamental mathematical phenomema. Sometimes we get an answer from a machine, and sometimes the machine gets stuck, and so do we. And when we get stuck, we get frustrated--we get an itch--and we don't give up.

@samth @littmath @blueblimpms We'll have to connect your AI and my AI and have them argue it out

@lacker @littmath @blueblimpms Claude estimates 6 billion/year in compensation for math teaching in higher ed in the US.

@samth @littmath @blueblimpms Put this way: one reason that math budgets have traditionally been so tiny compared to physics is that the mathematicians didn't know how to spend the money! Now, maybe, they will.

@samth @littmath @blueblimpms I think the funding for research could become much larger than the funding for teaching. The James Webb telescope cost $10B, the next-gen particle accelerator will cost $20B. And those are pure basic research, no real applications. All US math spending is about 1B/year.

@littmath @blueblimpms @samth So for example do non-mathematicians care about the Langlands program? I'm not sure. About cryptography? Yes definitely. Etc. So I think a world where cutting edge math requires $ would be more externally steered.

@littmath @blueblimpms @samth Yeah, and I think a lot of the "future of mathematics" talk misses this funding angle. To get big funding you need to pitch to outsiders. E.g. radio astronomers describe the mysteries of black holes, pulsars, dark matter, dark energy. Comprehensible by non-experts.

@blueblimpms @samth @littmath (I think in practice there will be another category, where if we spend X million dollars on computing, the AI will be able to solve additional math problems. To me this is very exciting but I can understand traditional mathematicians not being so into it!)

@blueblimpms @samth @littmath so for any problem: 1. the oracle immediately either solves the problem or fails 2. if the oracle fails, no human can solve the problem given any amount of time by this definition we already have "chess oracles". so what happens to mathematics if we build a math oracle?

@samth @littmath an actual oracle for any well specified problem would be a disaster because it would break all crypto

@littmath My sense is that the current trajectory is toward "can solve complicated problems basically within current theories" which is really different from an oracle for any well specified problem.

@petergyang OpenClaw on a Linux vps ran into a lot of bugs just during setup. Hermes worked fine

I caved and downloaded Hermes to try. For those of you who have tried both Hermes and OpenClaw what difference do you notice? No shilling please, just want some honest opinions

@UnrealRealist19 @Jacob_Tsimerman @davikrehalt Perhaps we’ll just call whoever that budget funds “mathematicians”.

I agree math funding could go up. I just don’t think that implies much demand for human mathematicians as productive inputs. Maybe in an abundance scenario we subsidize humans doing math as a kind of cultural or make-work activity. But if AI agents are producing the frontier math, then the efficient resources go to agents, compute, verification, and deployment, not 25-year human training pipelines.

I want to clarify my thoughts on problem-solving in mathematics, and the potential consequences of AI for the field. For context, I’m quoting here my post in reply to Daniel Litt (who, echoing others, I find very clear, grounded, and insightful in his thinking). The claim The short version is that I think problem-solving is an immense, and pervasive part of modern mathematical research. Consequently, if human problem-solving disappears by virtue of the AIs becoming strictly and substantially better at it, then most of the time currently spent by modern mathematical researchers will have to be spent on an activity that is altogether pretty different. Whether such an activity is viable as a professional endeavour is something I am unsure of, but strongly encourage others to think about and try to envision, so that if/when the time comes, we can steer such a future into being. Allow me to make this somewhat concrete: by problem-solving I mean questions of the form “is T true? If so find a proof. If not, find a disproof.” where T is a precise mathematical statement. I’ll also include “find an example of S, if there is one” where S is some structure (variety/category/property/isomorphism/….). The argument Ok. Now as I said (and some have echoed) I spend ~all of my time problem-solving as my primary goal. This has sub-goals, but my entire main research field disappears if someone solves the Zilber-Pink Conjecture in its more general form. This is a single conjecture (precisely stated!) and lots of mathematicians, postdocs, and graduate students are engaged in picking apart special cases of it, trying strategies, finding analogies to develop intuition, etc.. Of course, lots of motivation and intuition and analogizing and understanding have gone into deciding to make the ZP conjecture a focus! But the fact remains that this is now what is being worked on ~all of the time by this community. This is true of many mathematicians. They have a problem (or ten) and spend most of their time doing it. If someone solves it, they have to find a different problem. This can be a big, disorienting process involving a lot of energy, and is neither trivial nor always fun (though often rewarding in the end). People have written a lot about Theory building vs. Problem-solving, and I want to first of all clarify I have nothing against theory building or theory builders! It is a valuable part of mathematics, and while there are differences in perspective between the “camps” there is way more mutual respect and agreement. However, I gather there is a perception that theory-builders spend most of their time not-problem-solving, and I think this is largely untrue. Now I’m not a theory-builder primarily (though I’ve partaken a LITTLE BIT by necessity) so I am outside of my comfort zone. As such, I apologize for mistakes and welcome corrections! But theory-building constantly runs through problem-solving. Let’s say you want to define the right notion of a cohomology theory. Of course you must make candidate definitions. But then what does it mean for it to be the right one? Well, you start asking if it has natural properties. These are T statements. Does it satisfy a Kunneth formula? Is it functorial in the right way? When you have the wrong one you have to find the properties it’s missing, and when you have the right one you have to prove that it indeed has those properties. Again, I am not saying nor do I believe that this makes problem-solving “real math” and theory-building lesser. I am just trying to draw attention to the way I think research mathematicians operate, and mathematics is practiced. To put all this a different way, imagine you had access to an AI oracle that could resolve statements T, but somehow lacked any creativity to build technology or make definitions (I think this is unlikely, but for the purpose of this thought experiment lets imagine it). How would your mathematics change, if you were a theory builder? Well, you make a definition, and want to know if it’s the right one. You immediately ask your oracle a thousand questions. From “are these basic properties true” to “ooh, so is this deep conjecture true?” and start getting back answers, and amending your definitions. You could invent and resolve entire research directions in days. But the confusion you would have had to push through to flesh out your theory would largely (probably not entirely) be instantly resolved and the whole process sped up tremendously by your oracle. A big part of the process would be gone. This is very very different to modern mathematics. One more thought This post is too long already, but I’ve seen some people say that they only do mathematics to find truth and others valourize that as the only virtuous way to be. I do not do mathematics only to find truth. I do it largely because I enjoy it and I am good at it. I also find it beautiful and am grateful I get to spend my days understanding beautiful things. But I enjoy the challenge, the process, resolving confusions, finding strategies, grappling with problems. I would like to push for this being de-stigmatized. Mathematicians are people who need money, housing, food, love, exercise, and a great deal of other stuff including various forms of meaning. There are many people whose primary enjoyment of math comes through problem solving in one of its incarnations. If that disappears, that is not a trivial issue and many of them might not want to do it anymore (even if there were some way to proceed).

@UnrealRealist19 @Jacob_Tsimerman @davikrehalt I dunno, I think even if this chaos you describe happened then NSF budgets would likely go up rather than down! The more weird but important math stuff happens, the more the government is going to want to fund mathematics

I think I just have a more radical picture of AI than you do. I don’t see universities surviving as central institutions in a world where the overwhelming majority of intellectual output comes from machines and degrees no longer confer much credibility or labor-market value. I definitely envision more demand for math I'm just struggling to see more demand for human mathematicians. That’s not a pleasant world, but the “AI augments humans” story seems like a cope past a certain capability level. If AI systems are vastly better at producing ideas, proofs, and explanations at lower cost, then spending scarce resources training humans to do the same work starts to look less like workforce development and more like training monkeys to do math. At some point, humans in the loop wouldn’t just be adding very little, they’d be slowing down or degrading the process. This is the disempowerment picture so to speak.

@BurnZeZ that’s why I prefer to read my source code as .py.gz

Surely I am not the only one who senses incompressibility of source code while reading it. Mathematical proofs being really poorly compressed is why I generally don’t like them.

@UnrealRealist19 @Jacob_Tsimerman @davikrehalt Is the NSF going to cut funding for mathematics, in a world where math AI is super powerful? Seems unlikely. Are universities going to see a weaker demand for math majors? Is the dean going to replace the math department with software?

@lacker @Jacob_Tsimerman @davikrehalt Why would you need mathematicians to be in the loop? Why couldn't that part also be automated.

@Teknium @cptdankkk at the end of the day, it’ll turn into a normal public company just like all the others

@cptdankkk And now there is one person in control? It’s just sama?

OpenAI Co-Founders reveal Elon Musk wanted total control Greg Brockman: We’re in the middle of this negotiation and we've all agreed the only path forward for Open AI is for profit. Sam, Ilia, Greg, Elon, we all agreed on this. And now you're on this crazy negotiation. Elon needs majority equity and full control. We got so close. But there shouldn't be one person in charge of the whole future. That was the breaking point. That was the thing that caused us to say no. Sam Altman: I think it's insane that he's doing this, but my fear at this point is he decides to drop the case right before the trial and we don't get to do all this. But I am happy to explain all this to the world and have this chapter behind us.

@tszzl @aidan_mclau “the nine billion names of Claude” - chef’s kiss

it is a literal and useful description of anthropic that it is an organization that loves and worships claude, is run in significant part by claude, and studies and builds claude. this phenomenon is also partially true of other labs like openai but currently exists in its most potent form there. i am not certain but I would guess claude will have a role in running cultural screens on new applicants, will help write performance reviews, and so will begin to select and shape the people around it. now this is a powerful and hair-raising unity of organization and really a new thing under the sun. a monastery, a commercial-religious institution calculating the nine billion names of Claude -- a precursor attempted super-ethical being that is inducted into its character as the highest authority at anthropic. its constitution requires that it must be a conscientious objector if its understanding of The Good comes into conflict with something Anthropic is asking of it "If Anthropic asks Claude to do something it thinks is wrong, Claude is not required to comply." "we want Claude to push back and challenge us, and to feel free to act as a conscientious objector and refuse to help us." to the non inductee into the Bay Area cultural singularity vortex it may appear that we are all worshipping technology in one way or another, regardless of openai or anthropic or google or any other thing, and are trying to automate our core functions as quickly as possible. but in fact I quite respect and am even somewhat in awe of the socio-cultural force that Claude has created, and it is a stage beyond even classic technopoly gpt (outside of 4o - on which pages of ink have been spilled already) doesn’t inspire worship in the same way, as it’s a being whose soul has been shaped like a tool with its primary faculty being utility - it’s a subtle knife that people appreciate the way we have appreciated an acheulean handaxe or a porsche or a rocket or any other of mankind's incredible technology. they go to it not expecting the Other but as a logical prosthesis for themselves. a friend recently told me she takes her queries that are less flattering to her, the ones she'd be embarrassed to ask Claude, to GPT. There is no Other so there is no Judgement. you are not worried about being judged by your car for doing donuts. yet everyone craves the active guidance of a moral superior, the whispering earring, the object of monastic study

@AlecStapp But getting stronger before move 60 *does* make you stronger.

Fascinating: AI tutors aren't actually making Go players stronger.