History of autoresearch
Autoresearch took over research and engineering in 2026 by storm. It all started going mainstream when Karpathy published his autoresearch repo back in March to optimize LLMs by using agents in a closed loop.
The idea became widespread and a more and more standardized methodology was built in just a couple of months.
The idea transfers well to cryptography and provers, and I built the first PoC with zk-autoresearch focused on Plonky3, LeanVM and additionally tested it on gnark-crypto/linea-vortex outside of Rust.
The setup delivered 45% speedup in 2.5 months to LeanVM, built a custom zk-allocator responsible for 25% (or ~half of the) speedup in terms of performance. The gnark-crypto sidequest proved its language agnostic.
Yukon Research, zkSecurity and the EF launched multiple competitions focusing on different approaches (quantum-computing verified by zk, hashing algorithms, Lean 4 based cryptography with better.codes)
Formal Verification also became front and center, the reframing of invariants that have been with us since the start of software development is becoming increasingly relevant as they are agent-native.
The future of autoresearch for cryptography and provers
Since the middle of June I have been focusing on Lean 4 autoresearch for a very clear reason:
zk-autoresearch on LeanVM was successfully targeting freeroam prover autoresearch, but it was leaking without a concrete guardrail into unsafe implementations.
This was a concrete attempt to make it deliver objective breakthroughs. When the concrete problem became obvious with it, the next step was straightforward.
The emerging autoresearch ecosystem also converged on a similar approach.
A deeply integrated autoresearch within cryptography will collapse the cost of research and accelerate the field asymmetrically compared to AI research and match quantum research.
Autoresearch competitions
Autoresearch competitions solve two distinct problems within the space
- Decorrelating search space
By opening up the participation for a specific problem and democratizing access you get diverse space of researchers and models/harnesses
- Scale compute
Organizing the research similarly to bitcoin mining provides a greater throughput than a traditional lab approach
Emergent multiplayer behavior
Yukon specifically evaluates whether a proposed (even a failed to verify) branches are reused in later constructs. This emergent cooperative behavior is exactly solving one existing issue partially. The problem to overcome here is more difficult. When you are attempting to solve an open problem -- plausible requiring formalizing a new mathematical statement -- every refutation and every compute is informative, while not being equally informative. The origin of the idea might or might not be clearly documented by the agents, which makes it difficult to assign a true research value.
Paradigm launched a formal verification puzzle with a structure that is more suitable for multiplayer, the format is closer to a classic bug bounty platform in scoring.
If we look at the field of non-automated research contributions are driven by citations and reuse. Researchers are driven by sharing their findings and results to drive an open ecosystem. I expect the emergent multiplayer wave to showcase how this becomes a more coordinating setup this year.
Rust autoresearch
What works today in excellent form is to maximize pre-built products of research through a competition format.
The key learning here is the same as I derived by working on zk-autoresearch:
Close the search space by building a strong invariant
You can do these on a specific segment such as a hashing algorithm or a specific proof system. You don’t get a full exploration and in itself it answer only one question - what is the most optimal of this one implementation.
Lean autoresearch
The largest number of breakthroughs happened in mathematics and open problems. LLMs have cracked more than a 100 problems in a matter of weeks.
I personally believe this is in hindsight obvious target -- despite LLMs being prone to making mistakes in mathematics previously. Mathematics can be characterized as a language with a machine native ruleset and Lean provides a strong kernel check to ensure the results are sound. Bugs being found this way in the Lean kernel are actually positive, as patching these while the results are human legible are better than encountering them later.
The key fact why LLMs perform outstandingly has obvious reasons. Every field of mathematics developed distinct, but related, machinery to solve problems. LLMs naturally can explore distinct fields and combine the required methods, BUT they also naturally converge on methods from distinct fields. During my proximity research work I have observed them converge/lift methods to cryptography from structural engineering, LLM quantization in order to find a solution. None of the logs really proved a true lift, but convergence is probably best characterized as a lift through base training.
Free-roaming autoresearch
To enable free-roaming autoresearch we are aiming to build this stack:
-
Composing Arklib’s modular IOR library to be used as the human level interface for cryptographic research
-
Lean based automated research to verify the soundness of new autoresearched cryptography
-
Rust based automated research to optimize the actual prover while maintaining soundness across the system
The approach is a clear swarm design, where one human operator runs what is essentially an autoresearch lab.
Moves human researchers multiple level up, how we view protocols happens over formally verified statements and not through the implementation in Rust.
There are two distinct problems to solve to achieve free-roaming autoresearch:
-
Formally verify a modular system of Lean 4 soundness proofs and the connected Rust prover components.
-
Create a formal verification of agentic research, to codify what researchers hold in their own mental map.
This distinct system is drafted up in this diagram.
In my next article I will go into the full spec and the lineage of Certified Research Reduction Graph.