21 ms·

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

by konne88 11mo ago

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 11mo ago
> 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/ 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 11mo ago
  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.
  - spider-mario 11mo ago
    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.

by konne88 11mo ago

thaumasiotes 11mo ago

> 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/ 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 11mo ago
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.
- spider-mario 11mo ago
  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.