grantmaking.ai Launch Round
In this project, we aim to produce theoretical and foundational results in mechanistic interpretability by leveraging the recent advances in the mathematical abilities of frontier models. To make sure that the theorems provided by the frontier models do not contain logical flaws, we formally verify them in Lean 4. Preliminary analyses hint at a mathematical abstraction (imagine Feynman diagrams for particle physics and more recently, twistors for cosmological correlators) for multihead attention that can unlock progress in knowledge discovery for foundational mechanistic interpretability. Such an abstraction would help with tracking features across the layers of a transformer and hence provide theoretical foundations to build tools for feature discovery in transformers.
Pilot question
We start with a simple pilot question: how many attention heads are required to represent a Boolean function? We first treat multihead attention as a basic building block and then extend this analysis by including feed forward networks. By doing so, we are eventually working towards the goal of composing these component level theorems to understand the expressivity of the multilayer transformers. This question is not a purely abstract one: it grew out of my MATS work on understanding alignment pretraining, where I study how features are represented after an attention update. This connection gives some evidence that studying expressivity of multihead attention can be relevant to empirical mech interp, not just to formal expressivity theory.
The pilot question also serves as a feasibility test for the whole program. The setting is simple enough for frontier models to make progress while requiring a human expert to ask the high level questions. Initial autoresearch runs have produced impressive results that have provided us with some good intuitions that the next phase can build on.
Method
We plan to use an autoresearch pipeline, consisting of multiple frontier models collaborating to generate theorems and formally verify them. Our implementation adapts and extends the harness proposed in Numina Lean Agent, tailoring it to the problem at hand. During the course of the project, we hope to identify the "secret sauce" of multiagent orchestration, i.e., the optimal harness can make progress in foundational mech interp.
Who's involved?
The current team consists of 5 researchers with expertise in mechanistic interpretability and Lean formalization. We plan to onboard two additional researchers over the coming months to help with the multi agent orchestration and mech interp aspects of this project.
- Research lead: Karthik (myself). I am responsible for setting the research direction and coordinating the autoresearch pipeline among other things.
- Four mentees/collaborators from Berkeley Research Academy:
- Two paid mentees to be recruited:
- A research engineer to build the multi agent orchestration framework
- A research scientist to help with the mech interp aspects and guide the autoresearch framework
Concrete outputs
This phase is expected to run for four months, and I have requested the budget accordingly. By the end, we aim to deliver the following outputs:
- A mechanistic interpretability dojo: an open source modular library in Lean 4 that formally verifies the mathematical results obtained during this project. The goal is also for this to serve as a reusable codebase for other researchers to formally verify mathematical statements in mech interp.
- An open source multi agent orchestration harness: A system for coordinating frontier models for conjecture generation, proof search and Lean verification.
- LessWrong posts containing
- The theoretical progress made during the pilot, and
- A retrospective on what this project reveals about LLM-automated knowledge discovery for mechanistic interpretability.
Mechanistic interpretability is an important component of a broader toolkit for AI safety and oversight. Theoretical mech interp works (Elhage et al., 2021; Elhage et al., 2022) has shaped empirical interpretability by providing useful abstractions, and principled starting points for experimentation. However, developing this kind of theory has been demanding, requiring sustained expert effort to work through the underlying mathematics. Yet recent advances in language models for mathematical reasoning and formal theorem proving may make it possible to produce rigorous results at a lower cost. This project aims to produce foundational results for empirical interpretability by leveraging the growing mathematical abilities of frontier models, while identifying multi agent harnesses that make such theoretical research faster and more reliable.
Precedent for foundational theory shaping empirical mech interp research
There is precedent for foundational theory shaping mechanistic interpretability. "A Mathematical Framework for Transformer Circuits" (Elhage et al., 2021) worked out the mathematics of attention from first principles, and many later mechanistic interpretability ideas (for example, induction heads) build on that framework. Our aim is more modest than that of Elhage et al. but similar in spirit: a growing library of kernel-checked theorems that applied researchers can use as reference points, and a workflow for producing them faster than hand-derivation alone.
Why formally verified autoresearch for foundational theory?
1. Need for autoresearch: foundational theory is hard to scale with human effort alone. Hand-derivation is slow and expertise-intensive, and frontier models can now carry much of this load, and the field is already beginning to automate alignment research itself.
2. Need for formal verification: unverified automation can fail quietly. Frontier models make mistakes, long derivations accumulate subtle errors, and human evaluation alone cannot reliably catch either, so automated research tends to produce results that look compelling but are quietly wrong. Requiring every proof to pass the Lean kernel removes this failure mode for mathematical claims. Resolution's launch note makes a similar case: theory unlocks higher automation because proofs give automated research a source of ground truth that empirical metric-climbing lacks. A four-month open pilot that shows where kernel-verified autoresearch works, and where it breaks, is low-cost evidence for those far larger bets on automated alignment research.
De-risk: multi-agent framework for mech interp researchers
The project also studies which multi-agent workflows produce verified and successful research, which fail, and why. We will measure this on a live research problem and report the harness via an open source contribution. This also derisks the project: even if the head-complexity mathematics advances more slowly than hoped, the funded work still leaves behind an open, reusable multi-agent system for formalized interpretability theory.
Field-building
On the field building side, the project trains six early-career researchers (four dojo mentees already onboarded, two paid orchestration mentees to be recruited) at the intersection of interpretability, formal verification, and AI-assisted research, building a small talent pipeline for verified interpretability work.
Full budget with the split for the minimum and ideal: budget spreadsheet
The grant funds a four-month project (August to November 2026) with the following splits:
- Project lead stipend (part-time). I coordinate the project, adapt the proving agent to the head-complexity problem, supervise the mentees, and do the mathematics alongside the agents.
- Two paid mentees, a research scientist (mech interp theory) and a research engineer (multi-agent orchestration), who run the autoresearch experiments and the orchestration ablations. Paying them secures reliable commitment to the project's core deliverables.
- Claude, OpenAI, and Google AI subscriptions for the two paid mentees, since the multi-agent proving pipeline runs on frontier-model subscriptions.
- GPU compute for the empirical experiments (RunPod, roughly 10 hours per day across the project).
- CPU compute for the multi-agent orchestration runs and Lean proof checking (RunPod CPU pods, one each for me and the two paid mentees)