2 ms·
Would writing a Lean proof enable algorithmically searching for a shorter (simpler) proof?
by esafak 1y ago
Would writing a Lean proof enable algorithmically searching for a shorter (simpler) proof?
- agentcoops 1y agoI worked a long time ago on tools for algorithmically pruning proofs in another theorem-proving environment, Isabelle. That project was largely just using pretty straightforward graph algorithms, but I’m sure the state-of-the-art is much more advanced today (not least it’s an area where I assume LLMs would be helpful conjoined with formal methods).
- lgas 1y agoI'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide: theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := fun hpq : p ∧ q => have hp : p := And.left hpq have hq : q := And.right hpq show q ∧ p from And.intro hq hp To this: theorem and_commutative' (p q : Prop) : p ∧ q → q ∧ p := by exact fun a ↦ id (And.symm a) Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.