Email Gateway (Aug 25 2026 at 10:30): Email Gateway (Aug 25 2026 at 10:30):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
In another thread, Steven Obua <steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together with AI out of the box, just via invoking Isabelle from the command line. Formalisation work that I intended for several years now for abstraction logic I was able to complete within just 2 days in Isabelle/HOL, yielding 25K lines: the soundness and completeness of abstraction logic. This was done by just telling the AI to formalise what is in my book, and correcting some of the definitions it messed up. And beyond that, important additions to the logic such as additional proof rules, proving soundness and completeness with respect to them, and support for plurals; all designed, formalised, and proven correct within a matter of weeks.
Interactive theorem proving is really the killer app for AI, which is funny, because outside of ITP, most people are blissfully ignorant of what that even means, including all the big AI players, and inside of ITP, many seem reluctant rather than excited. I mean, formalising is now faster than thinking in many situations. They spent hundreds of billions of dollars to make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
Email Gateway (Aug 25 2026 at 10:57):From: Lawrence Paulson <lp15@cam.ac.uk>
In general, as the field progresses and tools improve, people are expected to be more ambitious and achieve more than before. What’s particularly difficult now is the rapid pace of change, coupled with the outsized role of money: those with more resources can afford the very best models and deliver more than people with modest resources. This is fundamentally unfair, but perhaps it is not a new problem.
Larry
On 25 Aug 2026 at 11:30 +0100, Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>, wrote:
In another thread, Steven Obua <steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together with AI out of the box, just via invoking Isabelle from the command line. Formalisation work that I intended for several years now for abstraction logic I was able to complete within just 2 days in Isabelle/HOL, yielding 25K lines: the soundness and completeness of abstraction logic. This was done by just telling the AI to formalise what is in my book, and correcting some of the definitions it messed up. And beyond that, important additions to the logic such as additional proof rules, proving soundness and completeness with respect to them, and support for plurals; all designed, formalised, and proven correct within a matter of weeks.
Interactive theorem proving is really the killer app for AI, which is funny, because outside of ITP, most people are blissfully ignorant of what that even means, including all the big AI players, and inside of ITP, many seem reluctant rather than excited. I mean, formalising is now faster than thinking in many situations. They spent hundreds of billions of dollars to make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
Email Gateway (Aug 25 2026 at 11:26):From: Alex Shkotin <alex.shkotin@gmail.com>
IMHO, It's one thing, like Steven Obua's case, when AI helps formalize
human inventions. It's quite another when AI itself conceives and proves a
theorem—then it's difficult to understand what it actually proved—a topic
for Terence Tao.
The value isn't in the length of the proof (like Fermat's theorem or the
Poincaré conjecture), but in how useful the proven result, i.e., the
theorem, is.
How can it be used?
And here, after all, we're not talking about a specific theorem, but about
the theory in which it emerged. How is this theory applied? What does a
proven theorem provide for applications of the theory?
Alex
вт, 25 авг. 2026 г. в 13:30, Gergely Buday <
cl-isabelle-users@lists.cam.ac.uk>:
In another thread, Steven Obua <steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together with
AI out of the box, just via invoking Isabelle from the command line.
Formalisation work that I intended for several years now for abstraction
logic I was able to complete within just 2 days in Isabelle/HOL, yielding
25K lines: the soundness and completeness of abstraction logic. This was
done by just telling the AI to formalise what is in my book, and correcting
some of the definitions it messed up. And beyond that, important additions
to the logic such as additional proof rules, proving soundness and
completeness with respect to them, and support for plurals; all designed,
formalised, and proven correct within a matter of weeks.Interactive theorem proving is really the killer app for AI, which is
funny, because outside of ITP, most people are blissfully ignorant of what
that even means, including all the big AI players, and inside of ITP, many
seem reluctant rather than excited. I mean, formalising is now faster than
thinking in many situations. They spent hundreds of billions of dollars to
make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
- Gergely
Email Gateway (Aug 25 2026 at 11:42):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
This is a multifaceted question.
Side note: I was also impressed by how efficient the process was, just
letting the AI use the installed Isabelle, with no integration. I had to
negotiate a bit about the workflow. In particular, Claude could not see
where the compilation diverges, so paradoxically, I did some mechanical
corrections manually that one would expect to be the computer's job
(like replacing "by blast" with "by metis" using try0). Here, some kind
of integration would help, and actually, Claude itself had some useful
ideas. However, this was a minor aspect of the whole project.
Another remarkable feature was that Claude was not very good at things I
considered obvious, and it often said something like "this is
combinatorics, you'd better tell me the right way to do this proof." So
this went against the news about solved Erdös conjectures and the like.
But of course, this depends crucially on the model strength and time spent.
A completely different story would be thousands of lines of new
proofs about topics never heard of. There is a lot of human-produced
garbage around in journals already (not only the predatory ones). AI can
speed up such a production beyond limits, for sure. However, the
positive effect may be that the question of whether the research makes
sense will become more obvious, given that the technical difficulty of
the proof can be easily outsourced (perhaps a slightly weird parallel:
nobody would admire you for being able to multiply two ten-digit numbers
as soon as calculators were invented).
Moreover, I cannot imagine how anybody can be prevented from using
tools that are available. Perhaps proving things without AI can become a
rare skill to display, something like starting a fire without matches.
Finally, I expect a big headache in teaching. I have just reviewed a
diploma thesis that is based on several papers, and the added value was
that the student implemented two algorithms and compared their
performance empirically. I suspect that the code could (and probably has
been) produced using AI, let alone that the whole thesis can probably be
produced just by feeding an agent the papers in question and the
assignment description.
Stepan
On 25-Aug-26 12:30 PM, Gergely Buday (via cl-isabelle-users Mailing
List) wrote:
In another thread, Steven Obua<steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together with AI out of the box, just via invoking Isabelle from the command line. Formalisation work that I intended for several years now for abstraction logic I was able to complete within just 2 days in Isabelle/HOL, yielding 25K lines: the soundness and completeness of abstraction logic. This was done by just telling the AI to formalise what is in my book, and correcting some of the definitions it messed up. And beyond that, important additions to the logic such as additional proof rules, proving soundness and completeness with respect to them, and support for plurals; all designed, formalised, and proven correct within a matter of weeks.
Interactive theorem proving is really the killer app for AI, which is funny, because outside of ITP, most people are blissfully ignorant of what that even means, including all the big AI players, and inside of ITP, many seem reluctant rather than excited. I mean, formalising is now faster than thinking in many situations. They spent hundreds of billions of dollars to make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
- Gergely
Email Gateway (Aug 25 2026 at 12:08):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Stepan,
I have been using Kevin Kappelman's link from Claude to Isabelle
(isabelle-pide-mcp) that he has advertised on this list and can report that I am
very happy with it. In particular, it mostly resolves the problem with Claude
not realizing that some proof step fails to terminate.
Tobias
On 25/08/2026 13:41, Stepan Holub (via cl-isabelle-users Mailing List) wrote:
This is a multifaceted question.
- This summer I had a similar experience like the one described by Steven:
talking to Claude I finally formalized two of my own old papers that were pretty
long and complex (in fact, some of my colleagues expressed doubts about the
correctness): lot of cases, lot of WLOGs (by reverse symmetry, by renaming
letters, by length argument), required ideas that I expected to take a lot of
trial and error to formalize in a convenient way (like using a pigeon hole
principle to reason about occurrences of factors in a word). In such a case, the
value is obvious, in my opinion. The corresponding thousands of lines are still
my old proof, but it is much better organized and beyond doubt. (Actually, just
one additional little gap I did not know about, easy to fix, was found.)Side note: I was also impressed by how efficient the process was, just letting
the AI use the installed Isabelle, with no integration. I had to negotiate a bit
about the workflow. In particular, Claude could not see where the compilation
diverges, so paradoxically, I did some mechanical corrections manually that one
would expect to be the computer's job (like replacing "by blast" with "by metis"
using try0). Here, some kind of integration would help, and actually, Claude
itself had some useful ideas. However, this was a minor aspect of the whole
project.Another remarkable feature was that Claude was not very good at things I
considered obvious, and it often said something like "this is combinatorics,
you'd better tell me the right way to do this proof." So this went against the
news about solved Erdös conjectures and the like. But of course, this depends
crucially on the model strength and time spent.
A completely different story would be thousands of lines of new proofs about
topics never heard of. There is a lot of human-produced garbage around in
journals already (not only the predatory ones). AI can speed up such a
production beyond limits, for sure. However, the positive effect may be that the
question of whether the research makes sense will become more obvious, given
that the technical difficulty of the proof can be easily outsourced (perhaps a
slightly weird parallel: nobody would admire you for being able to multiply two
ten-digit numbers as soon as calculators were invented).Moreover, I cannot imagine how anybody can be prevented from using tools that
are available. Perhaps proving things without AI can become a rare skill to
display, something like starting a fire without matches.Finally, I expect a big headache in teaching. I have just reviewed a diploma
thesis that is based on several papers, and the added value was that the student
implemented two algorithms and compared their performance empirically. I suspect
that the code could (and probably has been) produced using AI, let alone that
the whole thesis can probably be produced just by feeding an agent the papers in
question and the assignment description.Stepan
On 25-Aug-26 12:30 PM, Gergely Buday (via cl-isabelle-users Mailing List) wrote:
In another thread, Steven Obua<steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together with AI out
of the box, just via invoking Isabelle from the command line. Formalisation
work that I intended for several years now for abstraction logic I was able
to complete within just 2 days in Isabelle/HOL, yielding 25K lines: the
soundness and completeness of abstraction logic. This was done by just
telling the AI to formalise what is in my book, and correcting some of the
definitions it messed up. And beyond that, important additions to the logic
such as additional proof rules, proving soundness and completeness with
respect to them, and support for plurals; all designed, formalised, and
proven correct within a matter of weeks.Interactive theorem proving is really the killer app for AI, which is funny,
because outside of ITP, most people are blissfully ignorant of what that even
means, including all the big AI players, and inside of ITP, many seem
reluctant rather than excited. I mean, formalising is now faster than
thinking in many situations. They spent hundreds of billions of dollars to
make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
- Gergely
Email Gateway (Aug 25 2026 at 12:20):From: "Will J. Xu" <willxujun@hotmail.com>
I view the impact of AI on formalization as similar to its impact on mathematics - there is now an abundance of formalized proofs, just like there is a large swarth of AI-assisted mathematics paper submissions.
I believe AI-produced formal proofs carry the same research value as handwritten ones, but with the qualification that the (human) author should be responsible for the proof architecture. Roughly, that corresponds to a thorough familiarity with the formal proofs, and the ability to answer whatever technical query an outsider raises. If we lose grip on our formal proofs, a high-risk scenario can happen, where a subtle proof-assistant bug impacts a range of AI-produced proofs that few could explain. Having said that, proof assistant acts as a good shield against mathematical mistakes, so we are not in as precarious a position as mathematicians.
Nevertheless it is very exciting to hear that formal proofs can now be carried out with such high efficiency. I have a medium-scale formalization of logic in the works, with effort ongoing for ~ 1 year. I would be very willing to shorten the production cycle using AI - just have to make sure we understand the results carefully.
Jun
On 25 Aug 2026, at 6:30 PM, Gergely Buday <cl-isabelle-users@lists.cam.ac.uk> wrote:
In another thread, Steven Obua <steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together with AI out of the box, just via invoking Isabelle from the command line. Formalisation work that I intended for several years now for abstraction logic I was able to complete within just 2 days in Isabelle/HOL, yielding 25K lines: the soundness and completeness of abstraction logic. This was done by just telling the AI to formalise what is in my book, and correcting some of the definitions it messed up. And beyond that, important additions to the logic such as additional proof rules, proving soundness and completeness with respect to them, and support for plurals; all designed, formalised, and proven correct within a matter of weeks.
Interactive theorem proving is really the killer app for AI, which is funny, because outside of ITP, most people are blissfully ignorant of what that even means, including all the big AI players, and inside of ITP, many seem reluctant rather than excited. I mean, formalising is now faster than thinking in many situations. They spent hundreds of billions of dollars to make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
- Gergely
Email Gateway (Aug 25 2026 at 13:03):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
here are my two cents:
My main problem is related t AI relieving humans from doing proving
work: when doing proofs by hand becomes a "rare skill to display" (3),
we also loose a lot of understanding how proofs work, and how proofs
work at scale. You cannot design new proof/software engineering
methodologies if you don't have a good understanding of the problems you
are trying to solve. And the only proven and well-understood way to get
this understanding is doing it yourself. So, not only may we loose a
well-established teaching method to AI (4), but also a well established
research method to gain understanding of a problem and then come up with
new ideas.
Computer science has, obviously, used abstractions before. For example
when compilers where invented, most programmers stopped understanding
how to write assembly programs directly. Nowadays, programming directly
in assembly is, indeed, a rare skill to display. However, compilers, and
many other abstractions that we use, are very deterministic and
foreseeable. AI, on the other hand, is a very crude heuristics, that may
fail for reasons beyond understanding or logic.
So, abstract understanding of what a compiler does, such that we can
understand computer programs on a higher abstraction level, has a
different quality than abstract understanding of how to prompt an AI to
find a proof: The former builds on a deterministic and formal model of
how programs are translated, the latter very much depends on what
problems AI can currently solve and what not, which has no formal
explanation. So the best we can expect is to get a "feel" for which
proofs AI will complete, and which ones it won't. But without
understanding how proofs work (maybe not on the theorem prover syntactic
level, but on the mathematical level), we won't get further than "vibe
proving". And, similar, without understanding how correctness proofs for
large-scale software work, we will get stuck in the field at the state
were we are, unable to develop new methods and tools.
Obviously, another alternative is to loose interest in understanding how
things work, bet on AI becoming strictly more powerful than humans and
doing all the work for us, including invention of new methodology and
tools. In that scenario, we still must have an understanding of how
formal specifications work (unless we want to leave control and
responsibility to AI, too), but we don't need to understand any software
engineering or proof engineering. But we will loose complete control of
our proofs, code bases, code quality, etc, being at the mercy of AI (and
whoever controls it).
--
Peter
On 25/08/2026 12:41, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:
This is a multifaceted question.
- This summer I had a similar experience like the one described by
Steven: talking to Claude I finally formalized two of my own old
papers that were pretty long and complex (in fact, some of my
colleagues expressed doubts about the correctness): lot of cases, lot
of WLOGs (by reverse symmetry, by renaming letters, by length
argument), required ideas that I expected to take a lot of trial and
error to formalize in a convenient way (like using a pigeon hole
principle to reason about occurrences of factors in a word). In such a
case, the value is obvious, in my opinion. The corresponding thousands
of lines are still my old proof, but it is much better organized and
beyond doubt. (Actually, just one additional little gap I did not
know about, easy to fix, was found.)Side note: I was also impressed by how efficient the process was, just
letting the AI use the installed Isabelle, with no integration. I had
to negotiate a bit about the workflow. In particular, Claude could not
see where the compilation diverges, so paradoxically, I did some
mechanical corrections manually that one would expect to be the
computer's job (like replacing "by blast" with "by metis" using try0).
Here, some kind of integration would help, and actually, Claude itself
had some useful ideas. However, this was a minor aspect of the whole
project.Another remarkable feature was that Claude was not very good at things
I considered obvious, and it often said something like "this is
combinatorics, you'd better tell me the right way to do this proof."
So this went against the news about solved Erdös conjectures and the
like. But of course, this depends crucially on the model strength and
time spent.
A completely different story would be thousands of lines of new
proofs about topics never heard of. There is a lot of human-produced
garbage around in journals already (not only the predatory ones). AI
can speed up such a production beyond limits, for sure. However, the
positive effect may be that the question of whether the research makes
sense will become more obvious, given that the technical difficulty of
the proof can be easily outsourced (perhaps a slightly weird parallel:
nobody would admire you for being able to multiply two ten-digit
numbers as soon as calculators were invented).Moreover, I cannot imagine how anybody can be prevented from using
tools that are available. Perhaps proving things without AI can become
a rare skill to display, something like starting a fire without matches.Finally, I expect a big headache in teaching. I have just reviewed
a diploma thesis that is based on several papers, and the added value
was that the student implemented two algorithms and compared their
performance empirically. I suspect that the code could (and probably
has been) produced using AI, let alone that the whole thesis can
probably be produced just by feeding an agent the papers in question
and the assignment description.Stepan
On 25-Aug-26 12:30 PM, Gergely Buday (via cl-isabelle-users Mailing
List) wrote:In another thread, Steven Obua<steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together
with AI out of the box, just via invoking Isabelle from the command
line. Formalisation work that I intended for several years now for
abstraction logic I was able to complete within just 2 days in
Isabelle/HOL, yielding 25K lines: the soundness and completeness of
abstraction logic. This was done by just telling the AI to formalise
what is in my book, and correcting some of the definitions it messed
up. And beyond that, important additions to the logic such as
additional proof rules, proving soundness and completeness with
respect to them, and support for plurals; all designed, formalised,
and proven correct within a matter of weeks.Interactive theorem proving is really the killer app for AI, which
is funny, because outside of ITP, most people are blissfully
ignorant of what that even means, including all the big AI players,
and inside of ITP, many seem reluctant rather than excited. I mean,
formalising is now faster than thinking in many situations. They
spent hundreds of billions of dollars to make ITP really really
REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
- Gergely
Email Gateway (Aug 25 2026 at 14:05):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Well aware of how provocative the "rare skill to display" was, and also
well aware of the dangers Peter describes.
It all depends on what "doing proofs with AI" means. Based on the
recent experience I described, it means: a) keeping the proof process
structured, and b) thinking interactively.
Typical examples:
giving a rough description of the proof strategy, the agent would
answer: this means the following items 1. through 5., in item 3, I am
not sure how it will proceed. Should I first formalize the obvious
parts, or do you want to first analyze the dubious step three?
- asking the agent to formalize a given few lines argument from the
paper proof yields various outcomes:
often, the agent would suggest a simplification; I encountered both
possibilities: either the simplification is natural and helpful
(sometimes I would say: yes, that is what I actually had in mind, but
got lost), or the simplification is wrong (it ignores that the
simplified version does not work two paragraphs later). In the latter
case, the agent would then say: I made a mistake assuming so and so, but
it was wrong because that and this. Very often, this helps me to better
understand why exactly something has to be done as it is done.
a few genuine disagreements: several times the agent would say "the
user is insisting on this, let me dive deeper and see whether there is
something I am missing". And then it either finds the deeper reason, or
it will come with a detailed description of why doubts stay (and force
you to formulate precisely). Of course, one is easily bullied by an
agent insisting that one's idea is wrong. And of course, I was at least
once missing a subtle problem that would go unnoticed in paper reading.
(Something like: making the morphism simpler does not necessarily mean
making it shorter as the paper claims. So either the induction measure
has to be changed, or use another -- quite obvious, perhaps tacitly
assumed argument --, showing that the morphism is actually shorter too,
although not for the reason explicitly stated.)
And so on. Of course, formalization will not forgive you any of the
little gaps I have described, even without AI. However, finding out what
is wrong may take a week, instead of two minutes when using AI. The
hard-won experience after the week of struggles may be beneficial, but
not always.
Another metaphor comes to mind: playing blind chess is a rare skill to
display, and learning blind chess can help you a lot, chess-wise. But I
would not say that opening the eyes means that you stop being a chess
player.
Stepan
On 25-Aug-26 3:03 PM, Peter (via cl-isabelle-users Mailing List) wrote:
Dear list,
here are my two cents:
My main problem is related t AI relieving humans from doing proving
work: when doing proofs by hand becomes a "rare skill to display" (3),
we also loose a lot of understanding how proofs work, and how proofs
work at scale. You cannot design new proof/software engineering
methodologies if you don't have a good understanding of the problems
you are trying to solve. And the only proven and well-understood way
to get this understanding is doing it yourself. So, not only may we
loose a well-established teaching method to AI (4), but also a well
established research method to gain understanding of a problem and
then come up with new ideas.Computer science has, obviously, used abstractions before. For example
when compilers where invented, most programmers stopped understanding
how to write assembly programs directly. Nowadays, programming
directly in assembly is, indeed, a rare skill to display. However,
compilers, and many other abstractions that we use, are very
deterministic and foreseeable. AI, on the other hand, is a very crude
heuristics, that may fail for reasons beyond understanding or logic.So, abstract understanding of what a compiler does, such that we can
understand computer programs on a higher abstraction level, has a
different quality than abstract understanding of how to prompt an AI
to find a proof: The former builds on a deterministic and formal model
of how programs are translated, the latter very much depends on what
problems AI can currently solve and what not, which has no formal
explanation. So the best we can expect is to get a "feel" for which
proofs AI will complete, and which ones it won't. But without
understanding how proofs work (maybe not on the theorem prover
syntactic level, but on the mathematical level), we won't get further
than "vibe proving". And, similar, without understanding how
correctness proofs for large-scale software work, we will get stuck in
the field at the state were we are, unable to develop new methods and
tools.Obviously, another alternative is to loose interest in understanding
how things work, bet on AI becoming strictly more powerful than humans
and doing all the work for us, including invention of new methodology
and tools. In that scenario, we still must have an understanding of
how formal specifications work (unless we want to leave control and
responsibility to AI, too), but we don't need to understand any
software engineering or proof engineering. But we will loose complete
control of our proofs, code bases, code quality, etc, being at the
mercy of AI (and whoever controls it).--
Peter
On 25/08/2026 12:41, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:This is a multifaceted question.
- This summer I had a similar experience like the one described by
Steven: talking to Claude I finally formalized two of my own old
papers that were pretty long and complex (in fact, some of my
colleagues expressed doubts about the correctness): lot of cases, lot
of WLOGs (by reverse symmetry, by renaming letters, by length
argument), required ideas that I expected to take a lot of trial and
error to formalize in a convenient way (like using a pigeon hole
principle to reason about occurrences of factors in a word). In such
a case, the value is obvious, in my opinion. The corresponding
thousands of lines are still my old proof, but it is much better
organized and beyond doubt. (Actually, just one additional little gap
I did not know about, easy to fix, was found.)Side note: I was also impressed by how efficient the process was,
just letting the AI use the installed Isabelle, with no integration.
I had to negotiate a bit about the workflow. In particular, Claude
could not see where the compilation diverges, so paradoxically, I did
some mechanical corrections manually that one would expect to be the
computer's job (like replacing "by blast" with "by metis" using
try0). Here, some kind of integration would help, and actually,
Claude itself had some useful ideas. However, this was a minor aspect
of the whole project.Another remarkable feature was that Claude was not very good at
things I considered obvious, and it often said something like "this
is combinatorics, you'd better tell me the right way to do this
proof." So this went against the news about solved Erdös conjectures
and the like. But of course, this depends crucially on the model
strength and time spent.
A completely different story would be thousands of lines of new
proofs about topics never heard of. There is a lot of human-produced
garbage around in journals already (not only the predatory ones). AI
can speed up such a production beyond limits, for sure. However, the
positive effect may be that the question of whether the research
makes sense will become more obvious, given that the technical
difficulty of the proof can be easily outsourced (perhaps a slightly
weird parallel: nobody would admire you for being able to multiply
two ten-digit numbers as soon as calculators were invented).Moreover, I cannot imagine how anybody can be prevented from using
tools that are available. Perhaps proving things without AI can
become a rare skill to display, something like starting a fire
without matches.Finally, I expect a big headache in teaching. I have just reviewed
a diploma thesis that is based on several papers, and the added value
was that the student implemented two algorithms and compared their
performance empirically. I suspect that the code could (and probably
has been) produced using AI, let alone that the whole thesis can
probably be produced just by feeding an agent the papers in question
and the assignment description.Stepan
On 25-Aug-26 12:30 PM, Gergely Buday (via cl-isabelle-users Mailing
List) wrote:In another thread, Steven Obua<steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together
with AI out of the box, just via invoking Isabelle from the command
line. Formalisation work that I intended for several years now for
abstraction logic I was able to complete within just 2 days in
Isabelle/HOL, yielding 25K lines: the soundness and c
[message truncated]
Email Gateway (Aug 25 2026 at 14:34):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Another metaphor comes to mind: playing blind chess is a rare skill to
display, and learning blind chess can help you a lot, chess-wise. But
I would not say that opening the eyes means that you stop being a
chess player.
I would phrase this slightly differently: being able to play
grandmaster-level chess is a rare skill, but with the help of a
computer, everyone who knows the basic rules can beat Magnus Carlsen.
Stepan
On 25-Aug-26 3:03 PM, Peter (via cl-isabelle-users Mailing List) wrote:
Dear list,
here are my two cents:
My main problem is related t AI relieving humans from doing proving
work: when doing proofs by hand becomes a "rare skill to display"
(3), we also loose a lot of understanding how proofs work, and how
proofs work at scale. You cannot design new proof/software
engineering methodologies if you don't have a good understanding of
the problems you are trying to solve. And the only proven and
well-understood way to get this understanding is doing it yourself.
So, not only may we loose a well-established teaching method to AI
(4), but also a well established research method to gain
understanding of a problem and then come up with new ideas.Computer science has, obviously, used abstractions before. For
example when compilers where invented, most programmers stopped
understanding how to write assembly programs directly. Nowadays,
programming directly in assembly is, indeed, a rare skill to display.
However, compilers, and many other abstractions that we use, are very
deterministic and foreseeable. AI, on the other hand, is a very crude
heuristics, that may fail for reasons beyond understanding or logic.So, abstract understanding of what a compiler does, such that we can
understand computer programs on a higher abstraction level, has a
different quality than abstract understanding of how to prompt an AI
to find a proof: The former builds on a deterministic and formal
model of how programs are translated, the latter very much depends on
what problems AI can currently solve and what not, which has no
formal explanation. So the best we can expect is to get a "feel" for
which proofs AI will complete, and which ones it won't. But without
understanding how proofs work (maybe not on the theorem prover
syntactic level, but on the mathematical level), we won't get further
than "vibe proving". And, similar, without understanding how
correctness proofs for large-scale software work, we will get stuck
in the field at the state were we are, unable to develop new methods
and tools.Obviously, another alternative is to loose interest in understanding
how things work, bet on AI becoming strictly more powerful than
humans and doing all the work for us, including invention of new
methodology and tools. In that scenario, we still must have an
understanding of how formal specifications work (unless we want to
leave control and responsibility to AI, too), but we don't need to
understand any software engineering or proof engineering. But we will
loose complete control of our proofs, code bases, code quality, etc,
being at the mercy of AI (and whoever controls it).--
Peter
On 25/08/2026 12:41, Stepan Holub (via cl-isabelle-users Mailing
List) wrote:This is a multifaceted question.
- This summer I had a similar experience like the one described by
Steven: talking to Claude I finally formalized two of my own old
papers that were pretty long and complex (in fact, some of my
colleagues expressed doubts about the correctness): lot of cases,
lot of WLOGs (by reverse symmetry, by renaming letters, by length
argument), required ideas that I expected to take a lot of trial
and error to formalize in a convenient way (like using a pigeon hole
principle to reason about occurrences of factors in a word). In such
a case, the value is obvious, in my opinion. The corresponding
thousands of lines are still my old proof, but it is much better
organized and beyond doubt. (Actually, just one additional little
gap I did not know about, easy to fix, was found.)Side note: I was also impressed by how efficient the process was,
just letting the AI use the installed Isabelle, with no integration.
I had to negotiate a bit about the workflow. In particular, Claude
could not see where the compilation diverges, so paradoxically, I
did some mechanical corrections manually that one would expect to be
the computer's job (like replacing "by blast" with "by metis" using
try0). Here, some kind of integration would help, and actually,
Claude itself had some useful ideas. However, this was a minor
aspect of the whole project.Another remarkable feature was that Claude was not very good at
things I considered obvious, and it often said something like "this
is combinatorics, you'd better tell me the right way to do this
proof." So this went against the news about solved Erdös conjectures
and the like. But of course, this depends crucially on the model
strength and time spent.
A completely different story would be thousands of lines of new
proofs about topics never heard of. There is a lot of human-produced
garbage around in journals already (not only the predatory ones). AI
can speed up such a production beyond limits, for sure. However, the
positive effect may be that the question of whether the research
makes sense will become more obvious, given that the technical
difficulty of the proof can be easily outsourced (perhaps a slightly
weird parallel: nobody would admire you for being able to multiply
two ten-digit numbers as soon as calculators were invented).Moreover, I cannot imagine how anybody can be prevented from
using tools that are available. Perhaps proving things without AI
can become a rare skill to display, something like starting a fire
without matches.Finally, I expect a big headache in teaching. I have just
reviewed a diploma thesis that is based on several papers, and the
added value was that the student implemented two algorithms and
compared their performance empirically. I suspect that the code
could (and probably has been) produced using AI, let alone that the
whole thesis can probably be produced just by feeding an agent the
papers in question and the assignment description.Stepan
On 25-Aug-26 12:30 PM, Gergely Buday (via cl-isabelle-users Mailing
List) wrote:In another thread, Steven Obua<steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together
with AI out of the box, just via invoking Isabelle from the
command line. Formalisation work that I intended for several years
now for abstraction logic I was able to complete within just 2
days in Isabelle/HOL, yielding 25K lines: the soundness and
completeness of abstraction logic. This was done by just telling
the AI to formalise what is in my book, and correcting some of the
definitions it messed up. And beyond that, important additions to
the logic such as additional proof rules, proving soundness and
completeness with respect to them, and support for plurals; all
designed, formalised, and proven correct within a matter of weeks.Interactive theorem proving is really the killer app for AI, which
is funny, because outside of ITP, most people are blissfully
ignorant of what that even means, including all the big AI
players, and inside of ITP, many seem reluctant rather than
excited. I mean, formalising is now faster than thinking in many
situations. They spent hundreds of billions of dollars to make ITP
really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
- Gergely
Email Gateway (Aug 25 2026 at 16:31):From: Daniel Luckhardt <d.luckhardt@posteo.de>
In lieu of an essay I will just say the following (which has been said
before by someone I cannot name): A theory is only well understood when
all its proofs are simple.
Am 25.08.2026 12:30 schrieb Gergely Buday:
In another thread, Steven Obua <steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together with
AI out of the box, just via invoking Isabelle from the command line.
Formalisation work that I intended for several years now for
abstraction logic I was able to complete within just 2 days in
Isabelle/HOL, yielding 25K lines: the soundness and completeness of
abstraction logic. This was done by just telling the AI to formalise
what is in my book, and correcting some of the definitions it messed
up. And beyond that, important additions to the logic such as
additional proof rules, proving soundness and completeness with
respect to them, and support for plurals; all designed, formalised,
and proven correct within a matter of weeks.Interactive theorem proving is really the killer app for AI, which is
funny, because outside of ITP, most people are blissfully ignorant of
what that even means, including all the big AI players, and inside of
ITP, many seem reluctant rather than excited. I mean, formalising is
now faster than thinking in many situations. They spent hundreds of
billions of dollars to make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a
time to live in.My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review of the definition and theorem statements? I would love
to hear from people of this list on this.
- Gergely
Email Gateway (Aug 25 2026 at 16:42):From: M M <mihailsmilehins@gmail.com>
Dear All,
I could not resist replying to some of the comments in this thread, for
better or worse.
However, the positive effect may be that the question of whether the
research makes
sense will become more obvious, given that the technical difficulty of
the proof can be easily outsourced (perhaps a slightly weird parallel:
nobody would admire you for being able to multiply two ten-digit numbers
as soon as calculators were invented).
Who is to say that AI will not be able to propose/select better/more
important conjectures than humans? https://arxiv.org/abs/2409.04109.
Perhaps proving things without AI can become a
rare skill to display, something like starting a fire without matches.
Perhaps proving with AI can also become a rare skill to display once the
only query the AI agents will need is "Find and solve important problems in
mathematics/theoretical computer science, formalize results in a popular
proof assistant, propose topics for further work, write academic articles
suitable for publication in the best journals in the field, liaise with the
editors and reviewers to publish the articles.". This is where all of this
seems to be converging, and the pace is stunning:
https://openai.com/index/ten-advances-in-mathematics/.
Kind Regards,
Mihails Milehins
On Tue, Aug 25, 2026 at 9:33 AM Peter <cl-isabelle-users@lists.cam.ac.uk>
wrote:
Another metaphor comes to mind: playing blind chess is a rare skill to
display, and learning blind chess can help you a lot, chess-wise. But
I would not say that opening the eyes means that you stop being a
chess player.I would phrase this slightly differently: being able to play
grandmaster-level chess is a rare skill, but with the help of a
computer, everyone who knows the basic rules can beat Magnus Carlsen.Stepan
On 25-Aug-26 3:03 PM, Peter (via cl-isabelle-users Mailing List) wrote:
Dear list,
here are my two cents:
My main problem is related t AI relieving humans from doing proving
work: when doing proofs by hand becomes a "rare skill to display"
(3), we also loose a lot of understanding how proofs work, and how
proofs work at scale. You cannot design new proof/software
engineering methodologies if you don't have a good understanding of
the problems you are trying to solve. And the only proven and
well-understood way to get this understanding is doing it yourself.
So, not only may we loose a well-established teaching method to AI
(4), but also a well established research method to gain
understanding of a problem and then come up with new ideas.Computer science has, obviously, used abstractions before. For
example when compilers where invented, most programmers stopped
understanding how to write assembly programs directly. Nowadays,
programming directly in assembly is, indeed, a rare skill to display.
However, compilers, and many other abstractions that we use, are very
deterministic and foreseeable. AI, on the other hand, is a very crude
heuristics, that may fail for reasons beyond understanding or logic.So, abstract understanding of what a compiler does, such that we can
understand computer programs on a higher abstraction level, has a
different quality than abstract understanding of how to prompt an AI
to find a proof: The former builds on a deterministic and formal
model of how programs are translated, the latter very much depends on
what problems AI can currently solve and what not, which has no
formal explanation. So the best we can expect is to get a "feel" for
which proofs AI will complete, and which ones it won't. But without
understanding how proofs work (maybe not on the theorem prover
syntactic level, but on the mathematical level), we won't get further
than "vibe proving". And, similar, without understanding how
correctness proofs for large-scale software work, we will get stuck
in the field at the state were we are, unable to develop new methods
and tools.Obviously, another alternative is to loose interest in understanding
how things work, bet on AI becoming strictly more powerful than
humans and doing all the work for us, including invention of new
methodology and tools. In that scenario, we still must have an
understanding of how formal specifications work (unless we want to
leave control and responsibility to AI, too), but we don't need to
understand any software engineering or proof engineering. But we will
loose complete control of our proofs, code bases, code quality, etc,
being at the mercy of AI (and whoever controls it).--
Peter
On 25/08/2026 12:41, Stepan Holub (via cl-isabelle-users Mailing
List) wrote:This is a multifaceted question.
- This summer I had a similar experience like the one described by
Steven: talking to Claude I finally formalized two of my own old
papers that were pretty long and complex (in fact, some of my
colleagues expressed doubts about the correctness): lot of cases,
lot of WLOGs (by reverse symmetry, by renaming letters, by length
argument), required ideas that I expected to take a lot of trial
and error to formalize in a convenient way (like using a pigeon hole
principle to reason about occurrences of factors in a word). In such
a case, the value is obvious, in my opinion. The corresponding
thousands of lines are still my old proof, but it is much better
organized and beyond doubt. (Actually, just one additional little
gap I did not know about, easy to fix, was found.)Side note: I was also impressed by how efficient the process was,
just letting the AI use the installed Isabelle, with no integration.
I had to negotiate a bit about the workflow. In particular, Claude
could not see where the compilation diverges, so paradoxically, I
did some mechanical corrections manually that one would expect to be
the computer's job (like replacing "by blast" with "by metis" using
try0). Here, some kind of integration would help, and actually,
Claude itself had some useful ideas. However, this was a minor
aspect of the whole project.Another remarkable feature was that Claude was not very good at
things I considered obvious, and it often said something like "this
is combinatorics, you'd better tell me the right way to do this
proof." So this went against the news about solved Erdös conjectures
and the like. But of course, this depends crucially on the model
strength and time spent.
A completely different story would be thousands of lines of new
proofs about topics never heard of. There is a lot of human-produced
garbage around in journals already (not only the predatory ones). AI
can speed up such a production beyond limits, for sure. However, the
positive effect may be that the question of whether the research
makes sense will become more obvious, given that the technical
difficulty of the proof can be easily outsourced (perhaps a slightly
weird parallel: nobody would admire you for being able to multiply
two ten-digit numbers as soon as calculators were invented).Moreover, I cannot imagine how anybody can be prevented from
using tools that are available. Perhaps proving things without AI
can become a rare skill to display, something like starting a fire
without matches.Finally, I expect a big headache in teaching. I have just
reviewed a diploma thesis that is based on several papers, and the
added value was that the student implemented two algorithms and
compared their performance empirically. I suspect that the code
could (and probably has been) produced using AI, let alone that the
whole thesis can probably be produced just by feeding an agent the
papers in question and the assignment description.Stepan
On 25-Aug-26 12:30 PM, Gergely Buday (via cl-isabelle-users Mailing
List) wrote:In another thread, Steven Obua<steven.obua@gmail.com> wrote:
I must admit, I am blown away by how well Isabelle works together
with AI out of the box, just via invoking Isabelle from the
command line. Formalisation work that I intended for several years
now for abstraction logic I was able to complete within just 2
days in Isabelle/HOL, yielding 25K lines: the soundness and
completeness of abstraction logic. This was done by just telling
the AI to formalise what is in my book, and correcting some of the
definitions it messed up. And beyond that, important additions to
the logic such as additional proof rules, proving soundness and
completeness with respect to them, and support for plurals; all
designed, formalised, and proven correct within a matter of weeks.Interactive theorem proving is really the killer app for AI, which
is funny, because outside of ITP, most people are blissfully
ignorant of what that even means, including all the big AI
players, and inside of ITP, many seem reluctant rather than
excited. I mean, formalising is now faster than thinking in many
situations. They spent hundreds of billions of dollars to make ITP
really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
My colleague warned me that an AI generated proof might not be valued
in an academic evaluation, so the question is: where does research
value lie in using AI to generate thousands of lines of proofs? Is it
in the review o
[message truncated]
Last updated: Sep 02 2026 at 16:10 UTC