Dear readers, apologies for the infrequent updates. I am not a natural writer, and feel more natural as a researcher and builder. Recently, I have been busy building.

One update: I have recently joined Axiom. We built a prover that solved 12 out of 12 problems in the Putnam math competition, formalizing each proof in Lean. As a non-mathematician, it was cool witnessing our prover doing stuff far beyond my math and Lean abilities. We will continue to do awesome stuff, including in AI-assisted formal verification and verified code generation.

Meanwhile, I would like to mention a couple of recent projects.

ArtificialTheorems

The sister repo to ArtificialAlgorithms, ArtificialTheorems is a library of Lean 4 formalizations of theoretical foundations of AI and ML. Formalized results include:

  • convergence of stochastic gradient descent, including a formalization of the Robbins-Siegmund theorem from stochastic approximation theory.
  • Universal approximation theorem of neural networks.
  • Implicit regularization of gradient descent.
  • Theory of proper scoring rules.

As mentioned in my previous post, I am interested in formalizations of foundations of AI/ML, for similar motivations as my interest in verified code generation. In the near future, when our AI writes a paper on AI/ML research, I want to be able to ask it to formalize the theorems in Lean.

I realize that it is wildly optimistic to attempt this as a non-ML-theorist. But look at what’s already been formalized in this repo. This is already going beyond my knowledge of ML theory. But it becomes more feasible with the help of Codex and Claude Code.

As usual, comments, suggestions, contributions are appreciated!

VibeRegistry

If I can do this as a non-expert, imagine what true domain experts can do. Indeed, with the recent release of Anthropic and OpenAI models that are great at Lean, together with coding harnesses like Claude Code and Codex, we are beginning to see more and more autoformalization efforts by mathematicians, physicists, computer science and machine learning theorists.

On the other hand, many of them are relatively new to Lean, and perhaps not all are aware of the potential pitfalls of trusting an AI-produced Lean proof once it passed compilation.

In ArtificialTheorems, I have set up a template for robust verification: having a Specs directory containing just the theorem statements, then verifying the proofs against the specs using SafeVerify and Comparator. I have scripts that run these locally as well as in GitHub CI. I recommend anyone doing an autoformalization project to adopt a verification framework like this.

Later, I decided to create VibeRegistry, a registry of external autoformalization repos, that provides:

  • safe verification using SafeVerify and Comparator, using the setup outlined above.
  • a mechanism for human experts to sign off on the specs.

I added a few entries and plan to add more. Besides pure proofs, I am also interested in vibe-coded software libraries with correctness proofs. Please feel free to send in suggestions as GitHub issues!

With this, I am exploring a decentralized model of building libraries. As the registry expands, I plan to provide functionality to categorize, and to facilitate composition. Without a centrally enforced common set of definitions, this could potentially get messy. But perhaps our AIs will still figure it out.

Addendum, September 2026: VibeRegistry updates

Enough has changed since April that the description above is out of date. The main change: VibeRegistry now works as an overlay on two other registries, rather than only holding its own entries.

Palomar launched in August, signed by nine senior mathematicians and incubated by ICARM and the Lean FRO. It is a public record of Lean formalizations whose proofs have been machine-checked — deliberately arXiv-like infrastructure, not a journal — created as damage control against the current stream of loudly announced, poorly vetted machine-assisted proofs. LeanPool preserves Lean formalizations that do not fit Mathlib’s scope: 213 projects and over three million lines of Lean as I write this. In place of Mathlib’s high-bar human review it uses deterministic linters plus an LLM judgment of fit and significance, which lets it grow much faster while staying sorry-free and pinned to current Mathlib.

VibeRegistry now mirrors both: 390 upstream entries carrying some 1800 Lean statements, alongside the 30 in our own entries, all browsable and searchable at gasstationmanager.github.io/VibeRegistry. We do not re-verify their proofs; they already do that well. What we add on top is the human sign-off layer, through the same interface for a mirrored record as for one of our own entries.

Which brings me to why I keep insisting on that layer. Both registries are careful and explicit about the machine-checkable part. Both leave the one question a machine cannot settle — does this Lean statement actually say what the informal claim says? — to a language model. I understand the decision. It is the only part of the pipeline that does not scale.

I still think it is the wrong thing to automate, and better models would not change my mind. Formal verification is valuable to me as safety infrastructure precisely because it compresses what a human must check down to a single statement. The proof, the hundreds of lemmas, the tactic scripts: a machine can check all of it. That compression is the whole point. If we then hand the one surviving statement to a model as well, we have spent the compression and bought nothing back. The chain becomes: model writes the proof, model judges the statement, human reads a green checkmark. Nobody in it has formed a belief about what was proved.

Suppose the models become perfect at the judgment. I would still want a human name on that line. A guarantee no human has ever held is not one anyone can be accountable for, and the moment we will need it most is the moment AI is producing mathematics and code faster than we can read — exactly when giving up the last human-held link is most tempting and least recoverable. Sign-off stays optional in the registry, because a comparator-checked statement stands on its own. But it is the piece I would least like to hand over.

On the checking itself: Comparator is now the primary check. It rebuilds the proof in its own sandbox instead of trusting artifacts we produced, and it enforces the statement/proof separation against adversarial Lean. SafeVerify and lean4checker inspect artifacts our own build produced, so for the guarantee we publish they are redundant; both are now opt-in. Also opt-in is nanoda, an independent Lean kernel in Rust — a second kernel is cheap insurance against a bug in the first.