Heinzelmen public beta: browser-based automated proof search · Announcements

Stream: Announcements

Topic: Heinzelmen public beta: browser-based automated proof search

Yutaka Nagashima (Aug 16 2026 at 15:26):

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

No installation.
No setup.
No registration.
No subscription.
No API fees.

Just you and a .thy file with exactly one sorry.

Due to the severely 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 curious students who want to experiment with automated proof search without setting up a local environment.

We are also very 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.

Feedback, collaboration, and support are very welcome.

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

Enjoy!
Yutaka

Last updated: Sep 10 2026 at 03:40 UTC