Comment by agentcoops

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