[konne88]

I have proven quite a few theorems in Lean (and other provers) in my life, and the unfortunate reality is that for any non-trivial math, I still have to figure out the proof on paper first, and can only then write it in Lean. When I try to figure out the proof in Lean, I always get bogged down in details and loose sight of the bigger picture. Maybe better tactics will help. I'm not sure.

[thaumasiotes]

> Maybe better tactics will help. I'm not sure.

I don't see why they would.

If anyone is curious about the phenomenon, the second problem in session 7 at https://incredible.pm/ [ ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) ] is one where the proof is straightforward, but you're unlikely to get to it by just fooling around in the prover.

[practal]

In principle, LLMs can do this already. If you ask Claude to express this in simple words, you will get this translation of the theorem:

    "If applying f to things makes them red whenever they're not already red, then there must exist something that is red AND stays red after applying f twice to it."

Now the proof is easy to see, because it is the first thing you would try, and it works: If you have a red thing x, then either x and f(f(x)) are both red, or f(x) and f(f(f(x)) are both red. If x is not red, then f(x) is red. Qed.

You will be able to interact like this, instead of using tactics.