Stream: Announcements

Topic: ProofStudio

Yutaka Nagashima (Sep 27 2026 at 01:57):

Hi everyone!

I’d like to share ProofStudio, a browser-based workspace for Isabelle and other proof assistants:

https://proofstudio.org

ProofStudio gives curious newcomers a hands-on introduction to interactive theorem proving without local installation or setup. It combines examples, proof-state inspection, experimental proof search, and an AI assistant that can explain or edit proofs.

The current version is not intended to replace Isabelle/jEdit or support experts’ day-to-day work on substantial formalisation projects.

Its current limitations include:

• A single theory file at a time, rather than multi-file projects.
• A smaller set of editing and navigation features than a full IDE.
• Response times that can be slow.
• Limited server capacity for concurrent computational work.
• Technical glitches that still need addressing.

My long-term ambitions are to develop it into a platform with:

• A fully fledged proof editor and multi-file project support.
• Setup of substantial formalisations, such as AFP entries, RISC-V formalisation, and seL4, with just a few clicks.
• Integrated AI agents that assist with proof-development tasks, with resulting proofs checked by Isabelle.
• Proof search running on powerful cloud machines.
• Collections of educational materials and guided exercises, along the lines of an “Isabelle Mastering Marathon,” that learners can work through directly in the browser.

For the educational side, I would be particularly interested in hearing from anyone willing to share tutorials, exercises, or course materials under a permissive licence that allows adaptation and redistribution. Contributions and collaboration on new materials would also be very welcome.

We are currently short of resources, particularly computing capacity, which limits both proof automation and the default AI assistant. Support with compute, hosting, funding, or engineering would help, as would educational and research collaborations.

If you try it, I would appreciate feedback, especially on how well it serves beginners, along with bug reports and feature requests.

https://youtu.be/P4juSqvTTbY

Thanks!

Mathias Fleury (Sep 27 2026 at 05:36):

Please a default theory that acts as an example

Mathias Fleury (Sep 27 2026 at 05:37):

I wanted to try it, not to first find a theory on my hard drive and wondering what imports would work...

Mathias Fleury (Sep 27 2026 at 05:39):

ah there is an the example button

Mathias Fleury (Sep 27 2026 at 05:42):

too many line breaks for my taste

Yutaka Nagashima (Sep 28 2026 at 23:35):

@Mathias Fleury ,

Thanks for the feedback!
The fixes are on the way. I hope we can get them into the next release.

Last updated: Sep 30 2026 at 04:36 UTC