Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Browser-based automated proof search for Isabe...

Email Gateway (Aug 16 2026 at 15:35):

From: Yutaka Nagashima <united.reasoning@gmail.com>
Subject: [isabelle] Browser-based automated proof search for Isabelle/HOL

Dear Isabelle users,

I have finally launched Heinzelmen, a browser-based automated
theorem-proving service for Isabelle/HOL.

Service: https://heinzelmen.org
Demo video: https://www.youtube.com/watch?v=t1op9qOF1aU

• No installation.
• No setup.
• No registration.
• No subscription.
• No API fees.
• Just a .thy file with exactly one sorry.

Due to the limited computational resources currently available to us,
the public beta comes with several restrictions:

• one Isabelle/HOL .thy file;
• fewer than 500 LoC;
• exactly one sorry, which is replaced with a proof if search succeeds;
• Main only;
• no neural booster for proof search.

For this reason, I do not expect the current service to be
particularly useful to professional or experienced Isabelle users,
like many of you here. Rather, I hope it will be useful to Isabelle
beginners and struggling newcomers who want to experiment with
automated proof search without setting up a local environment.

We are interested in collaboration, for example, hosting other
automated proof-search engines, exploring support for other proof
assistants, or improving the computational resources available to the
service.

Enjoy!
Yutaka

Last updated: Sep 02 2026 at 16:10 UTC