Hacker News Reader

Comment by konne88 | Hacker News Reader

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.

View on HN

> 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.

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.

For anyone else for whom the justification for “either x and f(f(x)) are both red, or f(x) and f(f(f(x)) are both red” was not immediately obvious:

H: ∀x.(r(x)→⊥)→r(f(x))

goal: ∃x.r(x)∧r(f(f(x)))

If f(f(x)) is red:

    x is a solution (QED).

Otherwise:

    f(f(x)) not being red means f(x) must have been (by contraposition of H) and that f(f(f(x))) will be (by H); therefore, f(x) is a solution.

Reply on news.ycombinator.com