Email Gateway (Aug 02 2026 at 16:13): Email Gateway (Aug 02 2026 at 16:13):From: Mete Polat <mete@varto.ai>
Subject: [isabelle] Isabelle and Varto solve the complete PutnamBench mathematics benchmark
Hi everyone,
I am happy to announce that Varto, the Isabelle-based AI verification
platform we are building, has solved all the Isabelle PutnamBench problems:
https://trishullab.github.io/PutnamBench/leaderboard.html
The Putnam Mathematical Competition is an annual undergraduate mathematics
competition, and PutnamBench is a collection of its problems formalized for
theorem provers.
We also auto-formalized and proved all 32 additional problems previously
available only in Lean (this additional submission is currently under
review by the benchmark maintainers).
You can read more here: https://varto.ai/blog/putnambench/
I think this is a big win for Isabelle, especially since much of the
attention has focused on Lean until now.
It's an amazing feeling to go to bed and wake up finding that dozens of
cloud agents have completed a full verification work. We will soon release
our desktop and cloud platform we used for this. If you are interested in
being among the first to try it, please let me know. Your feedback would be
greatly appreciated!
We are also observing the beginnings of formally verifiable recursive
self-improvement in our internal software verification systems, and we are
excited to share more about this later this year. Turns out Isabelle is
great for this.
A few words about Varto: We are a Silicon Valley-based startup working to
bring autonomous, verifiable engineering to software, hardware, and
biology. We are hiring, so if you are interested in working at the
forefront of this technology, please DM me!
Incredible times ahead.
Best,
Mete
Email Gateway (Aug 05 2026 at 11:12):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] Isabelle and Varto solve the complete PutnamBench mathematics benchmark
Mete,
That's pretty cool, 640 right away! Putting Isabelle prominently on the map
which was dominated by Lean so far.
Putting Isabel prominently on the map which was dominated Eileen so far.
Thanks a lot, and I look forward to your emerging desktop and cloud platform.
Keep us posted!
Tobias
On 02/08/2026 18:02, Mete Polat wrote:
Hi everyone,
I am happy to announce that Varto, the Isabelle-based AI verification platform
we are building, has solved all the Isabelle PutnamBench problems:https://trishullab.github.io/PutnamBench/leaderboard.html
<https://trishullab.github.io/PutnamBench/leaderboard.html>
The Putnam Mathematical Competition is an annual undergraduate mathematics
competition, and PutnamBench is a collection of its problems formalized for
theorem provers.We also auto-formalized and proved all 32 additional problems previously
available only in Lean (this additional submission is currently under review by
the benchmark maintainers).You can read more here: https://varto.ai/blog/putnambench/ <https://varto.ai/
blog/putnambench/>I think this is a big win for Isabelle, especially since much of the attention
has focused on Lean until now.It's an amazing feeling to go to bed and wake up finding that dozens of cloud
agents have completed a full verification work. We will soon release our desktop
and cloud platform we used for this. If you are interested in being among the
first to try it, please let me know. Your feedback would be greatly appreciated!We are also observing the beginnings of formally verifiable recursive self-
improvement in our internal software verification systems, and we are excited to
share more about this later this year. Turns out Isabelle is great for this.A few words about Varto: We are a Silicon Valley-based startup working to bring
autonomous, verifiable engineering to software, hardware, and biology. We are
hiring, so if you are interested in working at the forefront of this technology,
please DM me!Incredible times ahead.
Best,
Mete
Last updated: Aug 12 2026 at 20:47 UTC