We at Protocol Snarkification - me and @alexanderlhicks, plus about 30 or so external collaborators - are working hard with formal verification to ship the highest-assurance zkVMs possible. (see end of thread for collaborators) (1/n)

Fantastic to have Rustan Leino join us at @HarmonicMath to help advance AI ✕ mathematics ✕ verification.

As we discussed with @VitalikButerin on our Fireside, formal verification is a big positive outcome from AI that will more than counterbalance the effects of AI finding new bugs. I am strongly supportive of math AI tools like Aristotle from @HarmonicMath driving this forward.

Today at the New York Number Theory Seminar, Wouter and Pietro were discussing their new paper. Really cool use of the AI-human feedback loop, with Aristotle as the main AI ingredient. I explained how I think formalization feels like doing the low-tech steps of algebraic geometry proofs with commutative algebra. You can have high-brow intuitions, but eventually one has to prove all the details. I wonder how this will evolve, but we are definitely at the level of assembly language being written by models like Aristotle. Tactics feel like the first glimpses of higher-level programming principles. The next step might be a more conversational style of working with the models. I am now working on a tighter integration of Lean with computer algebra languages. Stay tuned!

Here's what András Sárközy, Erdős's most prolific collaborator, asked 25 years ago: "How small can one make the maximal gap between the consecutive elements of a multiplicative Sidon set selected from {1, 2, ..., n}?" In particular: does there exist a multiplicative Sidon set A ⊆ {1, 2, …, n} such that every sub-interval of [1, n] of length at least √n contains at least one element of A? The answer is yes. The solution was autonomously discovered and formally verified in #Lean by Aristotle. We then improved the bound below √n and Aristotle formalised our proof too.

Interesting update: a few days ago, Nathanson presented a talk at the New York Number Theory Seminar explaining how Aristotle solved some of his problems.

Interesting update: a few days ago, Nathanson presented a talk at the New York Number Theory Seminar explaining how Aristotle solved some of his problems.

I think a radical new viewpoint is emerging on the many activities that mathematicians do. Perhaps a novel profession of mathematical engineering is emerging from the early chaos of AI for mathematics. I can see very clearly that the coordination, setup, technical pursuit, and orchestration of AI systems scaled for massive mathematical efforts and projects will require a special engineering mindset that is currently lacking, or almost completely absent, in mathematical projects. The existence of such a profession is not in opposition to mathematical tinkerers who use their artisanal craft to produce genuinely novel content. As with any kind of content, someone needs to adapt it to the grand scheme of things. This is why these roles are starting to appear complementary rather than competitive. Maybe this is a temporary activity, soon to be replaced by computers, but I think the major role of mathematical engineers will be to stay in touch with the tinkerers and provide a human cushion around their internal activities. I am enjoying this kind of activity (*), where you orchestrate with models and see how the project itself becomes a challenge in design and scale. This might well mean more jobs for mathematicians. In the long run, I suspect we may become secondary cognitive powers in parts of the mathematical information chain. But I do not think this will happen very soon across the whole system. And I hope it never happens at the most human layer: the joy people feel when a new idea is born. (*) This project is essentially a lambda-calculus lab, fully integrated with classical topics such as Church’s lambda calculus, the Aristotle formal proofs system, and extensions over particular papers. I presented it to students at the workshop in Warszawa-Falenty and was very pleased with the result. I am now using this framework for proof development. What strikes me most is that this is primarily an engineering challenge: the mathematics entering the pipeline is being handled, structured, and formalized, but not radically developed inside the pipeline itself.

To my mind, what seems most important here is not so much the results themselves, nor even the particular methods used in the proof. What really matters is the workflow: the closed loop from autonomous discovery of the right constructions, to formal verification of the proof in Lean, to informalised exposition back into a manuscript that mathematicians can read, understand, rewrite, and improve. It suggests a framework in which formal proof is not merely a static final certificate, but an active part of mathematical research: a medium through which ideas are found, organised, tested, explained and made available for human judgment. That dynamic loop is the real story for me. The natural next question is how far it can be pushed.

"Aristotle's proof is correct, simple, elegant, and beautiful. It uses techniques in the original paper and adds its own new ideas. I am amazed and impressed by what Aristotle has done." This is what Melvyn Nathanson, a leading additive number theorist and longtime Erdős collaborator, wrote to me after reading solutions by Aristotle (@HarmonicMath) to two problems he had posed earlier this year. Our paper answers Nathanson's Problems 10 and 11 on product intersection sets in semigroups, and also settles the second parts of Problems 4 and 7 as corollaries.

The Lean language (@leanprover) has utilities for verifying software, and AI is adept at using it. But can AI prove correctness for a *foreign architecture* with *no existing API*? It turns out, yes! @HarmonicMath's Aristotle wrote a z80 emulator: github.com/Timeroot/Z80Emu (1/n)

Write a lean model for this and prove it with @HarmonicMath

Kind of crazy. I had a rough idea for an Erdős problem, gave it to GPT-5.4 Pro, went for a walk, came back to a solution. I verified it, formalized it with Aristotle from @HarmonicMath together with @Tomodovodoo. Incredible how powerful these tools are in the right hands!

two major upgrades that made this possible asm2lean: assembly to Lean transpiler, no manual transcription hell aristotle by @HarmonicMath : the agentic prover can run for upto 24 hours on harder theorems x.com/HarmonicMath/status/20…