Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] ProofStudio: a browser-based workspace for Isa...

Email Gateway (Sep 29 2026 at 01:30):

From: Yutaka Nagashima <united.reasoning@gmail.com>
Subject: [isabelle] ProofStudio: a browser-based workspace for Isabelle and other proof assistants

Hi Isabeller users!

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

Website: https://proofstudio.org
Demo video: https://youtu.be/P4juSqvTTbY

ProofStudio gives curious newcomers a hands-on introduction to interactive
theorem proving without local installation.
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.

My long-term ambition is 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.

At the moment, we provide 10 examples adapted from Isabelle’s official
distributions for our environment.

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.

We are currently short of resources, particularly computing capacity, which
limits both proof automation and the default AI assistant.
Support with computational resources, 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.

Regards,
Yutaka

Email Gateway (Oct 01 2026 at 09:51):

From: Alex Shkotin <alex.shkotin@gmail.com>
Subject: [isabelle] ProofStudio: a browser-based workspace for Isabelle and other proof assistants

Hi Yutaka and All,

I would like to touch upon one aspect of "multi-file project support." This
resonates with my own proposal to store the framework of a theory—spanning
multiple natural and formal languages—in a single location. In this
approach, the units of knowledge constituting the theory (declarations of
primitive terms, definitions, axioms, theorems, and proofs) are stored as
discrete blocks, and specific blocks are selected for use as needed [1]. A
separate framework handles the storage of problems and their solutions [2].

While the logical organization of these repositories is fairly clear, the
physical implementation has not yet been decided.

It will be interesting to see which path you choose for your project, given
its multilingual nature.

Best regards,

Alex

[1] (PDF) Theory framework - knowledge hub message #1
<https://www.researchgate.net/publication/374265191_Theory_framework_-_knowledge_hub_message_1>

[2] Specific tasks of Ugraphia on a particular structure (formulations,
solutions, placement in the framework)
<https://www.researchgate.net/publication/380576198_Specific_tasks_of_Ugraphia_on_a_particular_structure_formulations_solutions_placement_in_the_framework>

вт, 29 сент. 2026 г. в 04:30, Yutaka Nagashima <united.reasoning@gmail.com>:

Hi Isabeller users!

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

Website: https://proofstudio.org
Demo video: https://youtu.be/P4juSqvTTbY

ProofStudio gives curious newcomers a hands-on introduction to interactive
theorem proving without local installation.
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.

My long-term ambition is 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.

At the moment, we provide 10 examples adapted from Isabelle’s official
distributions for our environment.

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.

We are currently short of resources, particularly computing capacity,
which limits both proof automation and the default AI assistant.
Support with computational resources, 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.

Regards,
Yutaka

Email Gateway (Oct 01 2026 at 14:20):

From: Yutaka Nagashima <united.reasoning@gmail.com>
Subject: [isabelle] ProofStudio: a browser-based workspace for Isabelle and other proof assistants

Hi Burkhart, Larry, and Alex,

Thanks for the feedback and encouragement!

Multi-file support is certainly on our roadmap.

At the moment, our plan is as follows:

-

Project structure: We plan to support the normal project/directory
structure used by each prover.

Since we support multiple ITPs we would rather respect the conventions
of each prover than introduce a ProofStudio-specific project structure.

Any prover-specific details should ideally be handled by the
corresponding prover integration rather than by ProofStudio itself.
-

Storage: We plan to rely primarily on external services such as
GitHub, Gitee, and Google Drive.

Since our own resources are quite limited, we do not think it would be
responsible or sustainable for ProofStudio to become a general-purpose
storage service for an unrestricted amount of user data.

We therefore plan to focus on integrating external storage services
rather than storing users' project files ourselves.

Personally, I would also be very interested in supporting open-source or
self-hosted storage solutions if there is demand from users.
-

Still undecided — AI/LLM data: We are still investigating how best to
handle the state and data associated with the AI component.

The current version lets users download their conversation logs as
Markdown, plain-text, or JSON files.

Once we introduce more comprehensive agentic AI support, we will
probably want a more robust way to preserve the interaction history and
working state so that users can return to ProofStudio after a break and
resume working with the AI from where they left off.

More broadly, the current development of ProofStudio is constrained mainly
by computational resources. At the moment, we have only two production
servers: one running the main service and another providing the default
LLM. If anyone is aware of suitable funding opportunities that could help
us overcome this limitation, I would be very interested to hear about them.

Although our immediate target is beginners, in the longer term I would also
like ProofStudio to support expert users who need substantial computational
resources. From what I can see, increasingly capable proof automation is
becoming increasingly compute-intensive, while most individual
theorem-proving researchers do not have access to large-scale
infrastructure of the kind available to private companies.

More generally, software development seems to be moving gradually from
computation performed entirely on researchers' or developers' own machines
toward cloud-based infrastructure that provides both computation and
higher-level services. I suspect theorem proving may move in a similar
direction.

Individual researchers are unlikely to be able to justify or maintain very
large computational infrastructure on their own, but perhaps we can pool
such resources collectively. There is some precedent for this in areas such
as numerical simulation, where shared academic infrastructure allows
researchers to retain meaningful control over their work rather than
becoming entirely dependent on private providers.

I think theorem proving should try to preserve the same kind of
independence. I would rather avoid a future in which a researcher has to
say:

"My account with Company XYZ was suspended for reasons I do not
understand, and as a result I can no longer realistically continue my
research."

This is why I think systems such as ProofStudio could matter beyond
providing a convenient browser interface. They could provide an open access
layer to pooled computational resources, allowing researchers to use
infrastructure from different academic or commercial providers without
becoming dependent on any single one.

Best,
Yutaka

On Thu, Oct 1, 2026 at 11:51 AM Alex Shkotin <alex.shkotin@gmail.com> wrote:

Hi Yutaka and All,

I would like to touch upon one aspect of "multi-file project support."
This resonates with my own proposal to store the framework of a
theory—spanning multiple natural and formal languages—in a single location.
In this approach, the units of knowledge constituting the theory
(declarations of primitive terms, definitions, axioms, theorems, and
proofs) are stored as discrete blocks, and specific blocks are selected for
use as needed [1]. A separate framework handles the storage of problems and
their solutions [2].

While the logical organization of these repositories is fairly clear, the
physical implementation has not yet been decided.

It will be interesting to see which path you choose for your project,
given its multilingual nature.

Best regards,

Alex

[1] (PDF) Theory framework - knowledge hub message #1
<https://www.researchgate.net/publication/374265191_Theory_framework_-_knowledge_hub_message_1>

[2] Specific tasks of Ugraphia on a particular structure (formulations,
solutions, placement in the framework)
<https://www.researchgate.net/publication/380576198_Specific_tasks_of_Ugraphia_on_a_particular_structure_formulations_solutions_placement_in_the_framework>

вт, 29 сент. 2026 г. в 04:30, Yutaka Nagashima <united.reasoning@gmail.com

:

Hi Isabeller users!

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

Website: https://proofstudio.org
Demo video: https://youtu.be/P4juSqvTTbY

ProofStudio gives curious newcomers a hands-on introduction to
interactive theorem proving without local installation.
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.

My long-term ambition is 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.

At the moment, we provide 10 examples adapted from Isabelle’s official
distributions for our environment.

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.

We are currently short of resources, particularly computing capacity,
which limits both proof automation and the default AI assistant.
Support with computational resources, 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.

Regards,
Yutaka

Email Gateway (Oct 01 2026 at 16:38):

From: Alex Shkotin <alex.shkotin@gmail.com>
Subject: [isabelle] ProofStudio: a browser-based workspace for Isabelle and other proof assistants

Hi Jutaka,

It’s a pity that a multilingual repository isn't currently in focus.

The idea is the creation of a storage system—perhaps similar to Wikipedia,
or rather DBpedia—but specifically designed for theories and problems.

Such a project could arguably be considered orthogonal to your engine, yet
it addresses a dimension you have already touched upon: how to store
knowledge accumulated by various provers in a uniform manner and "in one
place."

Here
<https://docs.google.com/spreadsheets/d/1gThpt1P8iulIl5SXfoekUiMg-562oiLfhHQYQjjg_y4/edit?usp=sharing>
is an example of a multilingual knowledge unit:

rus

Пусть A, B - точки
<https://docs.google.com/spreadsheets/d/1TB2Ntg3lxl3i0nPUlBg4HzarWYhJDjM2rk6leZtWS_M/edit?usp=drive_link>.
Если A и B различны то существует единственная прямая
<https://docs.google.com/spreadsheets/u/0/d/10GiUxSFsI7ALVIP6xzvoLKh3KbCxiE9i1radHWaTm-U/edit>
которая соединяет
<https://docs.google.com/spreadsheets/u/0/d/1OZmsnDR1jbo7oMCmkGD1g0ru7l8QGyT4yHuybrQw_rM/edit>
A с B.

eng

Let A and B be points. If A and B are distinct, then there exists a
unique straight
line that connects A to B.

yfl

∀p1,p2:Po p1≠p2 → (∃1l:SL connects(l p1 p2)).

coq <https://geocoq.github.io/GeoCoq/html/GeoCoq.Axioms.hilbert_axioms.html>

line_existence : ∀ A B, A ≠ B → ∃ l, Incid A l ∧ Incid B l;

line_uniqueness : ∀ A B l m, A ≠ B → Incid A l → Incid B l → Incid A m →
Incid B m → EqL l m;

cyc

???

vrm

???

cl

(forall (A B)

(if (and (point A) (point B) (not (= A B)))

(exists (l)

(and (line l)

(on A l)

(on B l)

(forall (m)

(if (and (line m) (on A m) (on B m))

(= l m)))))))

There is no Isabelle here, but I am ready to add:-)

Framework for Hilbert++ Geometry is here framework
<https://drive.google.com/drive/folders/1d3Bmi5sDq5_NoW47hQde3g2bpWkeqcnz>.

Best,

Alex

чт, 1 окт. 2026 г. в 17:20, Yutaka Nagashima <united.reasoning@gmail.com>:

Hi Burkhart, Larry, and Alex,

Thanks for the feedback and encouragement!

Multi-file support is certainly on our roadmap.

At the moment, our plan is as follows:

-

Project structure: We plan to support the normal project/directory
structure used by each prover.

Since we support multiple ITPs we would rather respect the conventions
of each prover than introduce a ProofStudio-specific project structure.

Any prover-specific details should ideally be handled by the
corresponding prover integration rather than by ProofStudio itself.
-

Storage: We plan to rely primarily on external services such as
GitHub, Gitee, and Google Drive.

Since our own resources are quite limited, we do not think it would be
responsible or sustainable for ProofStudio to become a general-purpose
storage service for an unrestricted amount of user data.

We therefore plan to focus on integrating external storage services
rather than storing users' project files ourselves.

Personally, I would also be very interested in supporting open-source
or self-hosted storage solutions if there is demand from users.
-

Still undecided — AI/LLM data: We are still investigating how best
to handle the state and data associated with the AI component.

The current version lets users download their conversation logs as
Markdown, plain-text, or JSON files.

Once we introduce more comprehensive agentic AI support, we will
probably want a more robust way to preserve the interaction history and
working state so that users can return to ProofStudio after a break and
resume working with the AI from where they left off.

More broadly, the current development of ProofStudio is constrained mainly
by computational resources. At the moment, we have only two production
servers: one running the main service and another providing the default
LLM. If anyone is aware of suitable funding opportunities that could help
us overcome this limitation, I would be very interested to hear about them.

Although our immediate target is beginners, in the longer term I would
also like ProofStudio to support expert users who need substantial
computational resources. From what I can see, increasingly capable proof
automation is becoming increasingly compute-intensive, while most
individual theorem-proving researchers do not have access to large-scale
infrastructure of the kind available to private companies.

More generally, software development seems to be moving gradually from
computation performed entirely on researchers' or developers' own machines
toward cloud-based infrastructure that provides both computation and
higher-level services. I suspect theorem proving may move in a similar
direction.

Individual researchers are unlikely to be able to justify or maintain very
large computational infrastructure on their own, but perhaps we can pool
such resources collectively. There is some precedent for this in areas such
as numerical simulation, where shared academic infrastructure allows
researchers to retain meaningful control over their work rather than
becoming entirely dependent on private providers.

I think theorem proving should try to preserve the same kind of
independence. I would rather avoid a future in which a researcher has to
say:

"My account with Company XYZ was suspended for reasons I do not
understand, and as a result I can no longer realistically continue my
research."

This is why I think systems such as ProofStudio could matter beyond
providing a convenient browser interface. They could provide an open access
layer to pooled computational resources, allowing researchers to use
infrastructure from different academic or commercial providers without
becoming dependent on any single one.

Best,
Yutaka

On Thu, Oct 1, 2026 at 11:51 AM Alex Shkotin <alex.shkotin@gmail.com>
wrote:

Hi Yutaka and All,

I would like to touch upon one aspect of "multi-file project support."
This resonates with my own proposal to store the framework of a
theory—spanning multiple natural and formal languages—in a single location.
In this approach, the units of knowledge constituting the theory
(declarations of primitive terms, definitions, axioms, theorems, and
proofs) are stored as discrete blocks, and specific blocks are selected for
use as needed [1]. A separate framework handles the storage of problems and
their solutions [2].

While the logical organization of these repositories is fairly clear, the
physical implementation has not yet been decided.

It will be interesting to see which path you choose for your project,
given its multilingual nature.

Best regards,

Alex

[1] (PDF) Theory framework - knowledge hub message #1
<https://www.researchgate.net/publication/374265191_Theory_framework_-_knowledge_hub_message_1>

[2] Specific tasks of Ugraphia on a particular structure (formulations,
solutions, placement in the framework)
<https://www.researchgate.net/publication/380576198_Specific_tasks_of_Ugraphia_on_a_particular_structure_formulations_solutions_placement_in_the_framework>

вт, 29 сент. 2026 г. в 04:30, Yutaka Nagashima <
united.reasoning@gmail.com>:

Hi Isabeller users!

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

Website: https://proofstudio.org
Demo video: https://youtu.be/P4juSqvTTbY

ProofStudio gives curious newcomers a hands-on introduction to
interactive theorem proving without local installation.
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.

My long-term ambition is 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.

At the moment, we provide 10 examples adapted from Isabelle’s official
distributions for our environment.

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.

We are currently short of resources, particularly computing capacity,
which limits both proof automation and the default AI assistant.
Support with computational resources, 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.

Regards,
Yutaka

Last updated: Oct 08 2026 at 21:07 UTC