Graph based History while proving

Stream: general

[Nadim Farhat]

Hi, I am very new to Lean . While I am learning and trying a few methods to prove equalities for example . I find myself mechanically iterating over different ways to prove something ( more like a brute force) and if I try different and multiple ways, sometimes I reach a point that I completely forget what I tried. Also, it seems the info view only displays steps to reach a goal in a linear manner; some proofs are not linear . So I was thinking to add another infoview ( maybe call it graphview) to record/log everything that have been tried and display step that led to accomplishing a goal and dead ends as a graph . Do you think such a feature is useful? is this already implemented ? Is someone currently implementing something similar, so I can tag along ? ( I got inspired from the MLops tools people use such as n8n and MLflow)

[Kenny Lau]

I think instead of writing a 100 line proof you can make a new lemma every time you reach a new step instead

[Kenny Lau]

and then the log you want will be the lemmas you separate out

[Anand Rao Tadipatri]

The PaperProof VS Code extension may be relevant: https://github.com/Paper-Proof/paperproof.

[Yaël Dillies]

This sounds a lot like what @Jovan Gerbscheid and others have developed with their boxproof thing

[Jovan Gerbscheid]

Hmm, it's not quite what boxproof is doing. But it's not clear to me exactly what you'd want to see in the graphview.

You say the info view displays steps to get to a goal in a linear manner. I think this is not quite right. The infoview only shows one step. And you can see the linear structure by moving the cursor through the proof script.

[Nadim Farhat]

now i have a clearer idea on what to do , maybe something like that https://askra.de/software/prooftree/ , is there a widget for that?