lgas a day ago

I'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.
Reply View 0 replies
agentcoops 3 days ago

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

Reply View 0 replies