Stream: General

Topic: Timed out proofs

Gergely Buday (Mar 14 2025 at 10:16):

Sometimes Sledgehammer gives an answer with a timeout:

(> 1.0 s, timed out)

What does this mean? When I click on the suggested one-liner, Isabelle/jEdit shows it in purple, and that means it is not an accepted proof by the kernel, possibly there is some looping.

What is a strategy to find an accepted proof? Sometimes it works that I copy the lemmas in the suggested one-liners into a using clause and then invoke Sledgehammer again. But this does not work always.

Shall I prove more intermediate lemmas?

Mathias Fleury (Mar 14 2025 at 10:25):

It means that sledgehammer tried the tactic for 1s and it did not finish

Mathias Fleury (Mar 14 2025 at 10:27):

There are a few possibilities:

- the proof method actually works, but it takes more time (but sledgehammer does not know that)
- the proof method actually does not work (taking forever), which is why sledgehammer is warning you about it

Mathias Fleury (Mar 14 2025 at 10:28):

Gergely Buday said:

Shall I prove more intermediate lemmas?

Exactly like if sledgehammer failed: you have to provide a proof by hand.

Mathias Fleury (Mar 14 2025 at 10:43):

Gergely Buday said:

What is a strategy to find an accepted proof? Sometimes it works that I copy the lemmas in the suggested one-liners into a using clause and then invoke Sledgehammer again. But this does not work always.

This way basically works if there is another way to find the proof. If this is an inherent problem (let's say a limitation of metis / an issue in smt), this will not solve the problem.

Gergely Buday (Mar 14 2025 at 10:45):

Thanks. Sometimes giving a longer timeout also works, but not in the case I face now.

Gergely Buday (Mar 14 2025 at 16:40):

@Mathias Fleury I have managed to prove the lemma.

The strategy was to give a calculational proof of three steps. For every step the search space was smaller than for the original lemma so Sledgehammer was able to find a proper one-liner proof.

I could visualise this as a square diagram where the square is created by the product of two transformations, and the original lemma was one side, while the calculational proof is going around on the other three sides.

Last updated: Apr 06 2025 at 01:43 UTC