adding heuristics to plausible

Stream: general

[Frederick Pu]

Is there any way we can use LLMs or other heuristics to help to find counter examples for plausible?

[Henrik Böving]

In principle you can overwrite the plausible instances to do more or less whatever you want I'd guess. Though especially with LLMs you might have better luck just posting the problem you're working on verbatim.

[Frederick Pu]

yeah but i want to be able to automatically check that the llms counter example is actually a valid counter example

[Henrik Böving]

I guess you could ask it to generate a script of the form

example (a b : Int) : a - b = b - a := by
  have : a = 10 := sorry
  have : b = -10 := sorry
  simp_all

and see if False pops out in your goal state

[Frederick Pu]

i wonder if there's a systematic way of generating a counter example template from a goal tho