kernel-rsi
RSI exmaple
An experiment where an AI agent rewrites its own proof-generating code to certify ever-larger prime numbers, verified step by step by the Lean theorem prover.
Kernel rsi is an experiment that tests whether an AI coding agent can improve its own code in a way that is actually verified as correct, rather than just claiming to improve. The project asks an AI agent to write a small Python program that proves a number is a prime number, with the proof checked by a separate tool called the Lean kernel. The agent is then allowed to rewrite its own program over and over, each time trying to prove a bigger prime number.
The key idea is that nothing here can be faked. Every proof the agent produces is independently rechecked by the Lean kernel, a program that either accepts a proof as valid or rejects it, with no partial credit and no shortcuts allowed. If the agent tries to cheat, its score simply becomes zero. This is different from many AI self improvement experiments, where success is judged by a fixed benchmark score that can sometimes be gamed. Here the target, the digit count of a certified prime, has no upper limit, so there is nothing for the agent to memorize in advance.
The experiment compared two approaches over 15 rounds. One let an AI agent read its own code and rewrite it to fix problems it found, and the other made small random changes to settings without any AI involved. Starting from a program that could certify a 128 digit prime, the AI powered version worked its way up to a 4096 digit prime, while the random mutation approach got stuck at 256 digits because it hit a structural limitation in the code that no simple setting could fix. The AI noticed the underlying code problem, rewrote it using a more efficient method, and kept improving from there.
The project requires Python and Lean 4, plus the Claude Code command line tool to run the AI powered condition. It includes scripts to verify the checking system itself is trustworthy, run either experimental condition, and regenerate the result charts. The repository is written mostly in Lean and currently has no stars on GitHub. It offers a plain look at how the two conditions behaved round by round, plus an explicit account of what the results do and do not prove about AI self improvement.
Where it fits
- Study whether AI self-improvement claims hold up under a rigorous, unforgeable verifier
- Compare an LLM-driven code rewriting loop against random parameter mutation
- Learn how a formal kernel can ground an AI agent's claims of progress
- Reproduce the prime certification experiment with a different proposer model