[isabelle] ATP Problem Encoding Issue · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] ATP Problem Encoding Issue

Email Gateway (Feb 23 2026 at 10:45):

From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>

Dear all,

For several problems in our development, we get a type error when we
try to call sledgehammer.

Minimal example of the type error with just standard Isabelle 2025-2
distribution:

<<
theory Scratch imports "HOL-Analysis.Analysis" begin
lemma bla: "retraction_map X Y f"
sledgehammer[prover=zipperposition,slices=1,max_facts=1]

>

The issue boils down to different Isabelle variables being encoded as
a single variable (name capture), the isabelle fact
retraction_map_def:

∃g. retraction_maps ?X ?Y ?f g

becomes:

∃X. retraction_maps X Y f X

Which does not typecheck as the second X having a different type than
the first one. This happens for several other problems and encodings,
affecting some slices for Vampire and others.

Cheers,
Cezary

Email Gateway (Feb 23 2026 at 11:50):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>

Dear Cezary,

This is a very serious issue. Thank you for the report. We will investigate and come back to you.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 23. Feb 2026, at 11:45, Cezary Kaliszyk <cezarykaliszyk@gmail.com> wrote:

Dear all,

For several problems in our development, we get a type error when we
try to call sledgehammer.

Minimal example of the type error with just standard Isabelle 2025-2
distribution:

<<
theory Scratch imports "HOL-Analysis.Analysis" begin
lemma bla: "retraction_map X Y f"
sledgehammer[prover=zipperposition,slices=1,max_facts=1]

>

The issue boils down to different Isabelle variables being encoded as
a single variable (name capture), the isabelle fact
retraction_map_def:

∃g. retraction_maps ?X ?Y ?f g

becomes:

∃X. retraction_maps X Y f X

Which does not typecheck as the second X having a different type than
the first one. This happens for several other problems and encodings,
affecting some slices for Vampire and others.

Cheers,
Cezary

smime.p7s

Email Gateway (Feb 24 2026 at 10:58):

From: Benjamin Puyobro <cl-isabelle-users@lists.cam.ac.uk>

Dear all,

I don't know if my issue is related or not to the previously mentionned
issue by Cezary:

I've also noticed a weird behavior from sledgehammer, proof that were
rather easily found by sledgehammer (especially smt ones) are not found
anymore by sledgehammer in Isabelle2025-2. Here is a minimal example to
reproduce the issue:

theory Scratch
imports Main HOL.Real
begin

locale test =
fixes N ::nat
assumes ‹N > 0›
fixes f::"nat ⇒ real"
assumes a0: ‹∀i∈{0..N}. f i > 0›
begin
lemma travelled_less_than:
assumes
h:‹i∈{0..N}›
"0 < (t::real)"
"0 ≤ s"
"t < T"
"a ≤ f i"
shows
"a * (t * (t * 2)) + t * (s * 4)
< f i * (T * (T * 2)) + T * (s * 4)"
proof -
have ‹a * t ≤ f i *t›
using h by(auto simp:field_simps)
moreover have ‹a * t ≤ f i *T›
proof -
have ‹f i *T ≥ f i * t›
using h a0 by(auto simp:algebra_simps)
thus ?thesis using calculation by auto
qed
moreover have ‹2* s + a * t < 2* s + f i *T›
using calculation a0
using h mult_less_cancel_left_pos
by (metis add_less_cancel_left order_less_le order_less_trans)
moreover have ‹t2 s + t*a * t < T2 s + f i *T * T›
using calculation h sledgehammer (* In isabelle 2025 sledgehammer
would find the following smt instantaneously, it is not found here. *)
by (smt (verit, ccfv_SIG) a0 mult.commute mult_le_cancel_right
mult_pos_pos mult_strict_mono)
ultimately show ?thesis by(auto simp:field_simps)
qed
end

In this example, if you provide a0 in the context: "using ... a0
sledgehammer" then it will find the proof, but then if you change the
import HOL.Real by HOL-Analysis.Finite_Cartesian_Product it won't find
the proof anymore.

I also have more complex examples (not involving facts declared in a
locale) that can't be reduced to a minimal example in which even with
the context provided sledgehammer won't find anything.

Best,
Benjamin

Le 2026-02-23 12:50, Jasmin Blanchette a écrit :

Dear Cezary,

This is a very serious issue. Thank you for the report. We will
investigate and come back to you.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 23. Feb 2026, at 11:45, Cezary Kaliszyk
<cezarykaliszyk@gmail.com> wrote:

Dear all,

For several problems in our development, we get a type error when we
try to call sledgehammer.

Minimal example of the type error with just standard Isabelle 2025-2
distribution:

<<
theory Scratch imports "HOL-Analysis.Analysis" begin
lemma bla: "retraction_map X Y f"
sledgehammer[prover=zipperposition,slices=1,max_facts=1]

The issue boils down to different Isabelle variables being encoded as
a single variable (name capture), the isabelle fact
retraction_map_def:

∃g. retraction_maps ?X ?Y ?f g

becomes:

∃X. retraction_maps X Y f X

Which does not typecheck as the second X having a different type than
the first one. This happens for several other problems and encodings,
affecting some slices for Vampire and others.

Cheers,
Cezary

Email Gateway (Feb 24 2026 at 17:02):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>

Dear Benjamin,

In this example, if you provide a0 in the context: "using ... a0 sledgehammer" then it will find the proof, but then if you change the import HOL.Real by HOL-Analysis.Finite_Cartesian_Product it won't find the proof anymore.

These behaviors arise because the imports influence which lemmas get selected, and that influences proof search in various ways. So a priori, nothing of what you report is abnormal.

Best,
Jasmin

On 24. Feb 2026, at 11:57, Benjamin Puyobro (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:

Dear all,

I don't know if my issue is related or not to the previously mentionned issue by Cezary:

I've also noticed a weird behavior from sledgehammer, proof that were rather easily found by sledgehammer (especially smt ones) are not found anymore by sledgehammer in Isabelle2025-2. Here is a minimal example to reproduce the issue:

theory Scratch
imports Main HOL.Real
begin

locale test =
fixes N ::nat
assumes ‹N > 0›
fixes f::"nat ⇒ real"
assumes a0: ‹∀i∈{0..N}. f i > 0›
begin
lemma travelled_less_than:
assumes
h:‹i∈{0..N}›
"0 < (t::real)"
"0 ≤ s"
"t < T"
"a ≤ f i"
shows
"a * (t * (t * 2)) + t * (s * 4)
< f i * (T * (T * 2)) + T * (s * 4)"
proof -
have ‹a * t ≤ f i *t›
using h by(auto simp:field_simps)
moreover have ‹a * t ≤ f i *T›
proof -
have ‹f i *T ≥ f i * t›
using h a0 by(auto simp:algebra_simps)
thus ?thesis using calculation by auto
qed
moreover have ‹2* s + a * t < 2* s + f i *T›
using calculation a0
using h mult_less_cancel_left_pos
by (metis add_less_cancel_left order_less_le order_less_trans)
moreover have ‹t2 s + t*a * t < T2 s + f i *T * T›
using calculation h sledgehammer (* In isabelle 2025 sledgehammer would find the following smt instantaneously, it is not found here. *)
by (smt (verit, ccfv_SIG) a0 mult.commute mult_le_cancel_right mult_pos_pos mult_strict_mono)
ultimately show ?thesis by(auto simp:field_simps)
qed
end

In this example, if you provide a0 in the context: "using ... a0 sledgehammer" then it will find the proof, but then if you change the import HOL.Real by HOL-Analysis.Finite_Cartesian_Product it won't find the proof anymore.

I also have more complex examples (not involving facts declared in a locale) that can't be reduced to a minimal example in which even with the context provided sledgehammer won't find anything.

Best,
Benjamin

Le 2026-02-23 12:50, Jasmin Blanchette a écrit :

Dear Cezary,
This is a very serious issue. Thank you for the report. We will
investigate and come back to you.
Best,
Jasmin
--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 23. Feb 2026, at 11:45, Cezary Kaliszyk
<cezarykaliszyk@gmail.com> wrote:
Dear all,
For several problems in our development, we get a type error when we
try to call sledgehammer.
Minimal example of the type error with just standard Isabelle 2025-2
distribution:
<<
theory Scratch imports "HOL-Analysis.Analysis" begin
lemma bla: "retraction_map X Y f"
sledgehammer[prover=zipperposition,slices=1,max_facts=1]
The issue boils down to different Isabelle variables being encoded as
a single variable (name capture), the isabelle fact
retraction_map_def:
∃g. retraction_maps ?X ?Y ?f g
becomes:
∃X. retraction_maps X Y f X
Which does not typecheck as the second X having a different type than
the first one. This happens for several other problems and encodings,
affecting some slices for Vampire and others.
Cheers,
Cezary

smime.p7s

Email Gateway (Mar 09 2026 at 16:40):

From: Martin Desharnais-Schäfer <martin.desharnais-schaefer@posteo.de>

Hi Cezary,

I investigated and produced the following commit that should fix the issue:

changeset: 84111:4e9d0630991b
user: desharna
date: Tue Feb 24 10:48:01 2026 +0100
summary: fixed name clash during eta expansion in Sledgehammer's
TPTP generation

Cheers,
Martin

On 2/23/26 12:50, Jasmin Blanchette wrote:

Dear Cezary,

This is a very serious issue. Thank you for the report. We will
investigate and come back to you.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 23. Feb 2026, at 11:45, Cezary Kaliszyk <cezarykaliszyk@gmail.com>
wrote:

Dear all,

For several problems in our development, we get a type error when we
try to call sledgehammer.

Minimal example of the type error with just standard Isabelle 2025-2
distribution:

<<
theory Scratch imports "HOL-Analysis.Analysis" begin
lemma bla: "retraction_map X Y f"
sledgehammer[prover=zipperposition,slices=1,max_facts=1]

>

The issue boils down to different Isabelle variables being encoded as
a single variable (name capture), the isabelle fact
retraction_map_def:

∃g. retraction_maps ?X ?Y ?f g

becomes:

∃X. retraction_maps X Y f X

Which does not typecheck as the second X having a different type than
the first one. This happens for several other problems and encodings,
affecting some slices for Vampire and others.

Cheers,
Cezary

Email Gateway (Mar 10 2026 at 18:14):

From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>

Hi Martin,

Great, thanks, this works indeed!
We have found one more name clash in Sledgehammer. It is of similar
kind but it is already in Isabelle and is just exposed by
sledgehammer.

Simplest way to reproduce. In any recent Isabelle (e.g. Isabelle
2025-2, happens also with your eta-renaming fix backported)
load Nominal/Examples/Class.thy and go to line 720 and type:
sledgehammer[prover=zipperposition,slices=1,max_facts=1]

Details: There are two free variables 'd' with different types (one is
a 'name' and one is a 'coname') which causes a typing error.

Most Isabelle tactics seem to work with two variables named the same
way, in fact the goals are proved successfully but sledgehammer does
not produce valid files and fails. Is this something you can also help
with?

Cheers,
Cezary

On Tue, Mar 10, 2026 at 3:40 AM Martin Desharnais-Schäfer
<martin.desharnais-schaefer@posteo.de> wrote:

Hi Cezary,

I investigated and produced the following commit that should fix the issue:

changeset: 84111:4e9d0630991b
user: desharna
date: Tue Feb 24 10:48:01 2026 +0100
summary: fixed name clash during eta expansion in Sledgehammer's
TPTP generation

Cheers,
Martin

On 2/23/26 12:50, Jasmin Blanchette wrote:

Dear Cezary,

This is a very serious issue. Thank you for the report. We will
investigate and come back to you.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 23. Feb 2026, at 11:45, Cezary Kaliszyk <cezarykaliszyk@gmail.com>
wrote:

Dear all,

For several problems in our development, we get a type error when we
try to call sledgehammer.

Minimal example of the type error with just standard Isabelle 2025-2
distribution:

<<
theory Scratch imports "HOL-Analysis.Analysis" begin
lemma bla: "retraction_map X Y f"
sledgehammer[prover=zipperposition,slices=1,max_facts=1]

>

The issue boils down to different Isabelle variables being encoded as
a single variable (name capture), the isabelle fact
retraction_map_def:

∃g. retraction_maps ?X ?Y ?f g

becomes:

∃X. retraction_maps X Y f X

Which does not typecheck as the second X having a different type than
the first one. This happens for several other problems and encodings,
affecting some slices for Vampire and others.

Cheers,
Cezary

Last updated: Mar 14 2026 at 08:38 UTC