Viewing proof state in documentation?

Stream: Is there code for X?

[max]

I wrote some lean code yesterday and posted it to GitHub. I see the docs works. https://anandijain.github.io/ProofsWMathlib.lean/docs/ProofsWMathlib/Lean/day_2025_12_30.html.

What I'm wondering is if there is a way that the compiler could cache the intermediate goal states so that I could interact with the proof in the documentatipn, without needing a full VSCode. This would be handy for reading formal proofs from others without needing to clone the repo. I believe it should be possible because it's not requiring the compiler itself, just a record of the changes to the state. I don't know anything about the internals, however.

Is this possible? Thanks!

[Snir Broshi]

Hover over the small ellipses in this, is that what you mean?
You can also click the small ellipses in this and this and see the goal state on the right (that tool also tries to translate Lean to natural language, but that part can be removed).
Also I think this message refers to exactly what you want.
I only know of these results, idk how they were generated

[Ilmārs Cīrulis]

It's Verso.

From the https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

The Lean proofs are rendered using Verso, which allows the goal state (the proof progress) to be inspected before and after each "tactic".

[runofff]

image.png
Thank you both! I decided neither of those options was quite what I wanted. I decided to implement my own.

Here you can view a toy project https://anandijain.github.io/DocTest3.lean/docs/DocTest3/Basic.html and look for the link to "traces", which allows you to explore the static proof traces online without needing to start an instance of the LSP yourself.

Basically the way this works is I start a language server then open up lean source files and query every cursor position for the LSP plainGoal command.

One neat aspect of this project was the CI https://github.com/anandijain/DocTest3.lean/blob/main/.github/workflows/lean_action_ci.yml

I was able to use regex to insert a link to the generated html proof viewer. A second iteration of the project would be to rewrite this natively in Lean for performance and also to avoid some hacks that allowed me to modify the generated documentation.

[Snir Broshi]

Cool! But isn't this exactly the same as what Verso does just with a different html? Isn't it easier to just modify the Verso html?

[Snir Broshi]

Also, are you related to the OP?

[max]

yes, sorry. I forgot the password to that other account. I probably could modify verso but this was quite easy to vibecode just using the LSP.

[max]

Oh apparently on mobile I'm logged into the original account

[max]

I guess my question is why doesn't doc-gen4 then have a way to use verso to emit proof state traces in the static documentation. That is the feature that I wanted to address

[Kevin Buzzard]

(@max @runofff it's against the rules of this site to have two accounts -- can you please deactivate one?)

[runofff]

done. sorry

[Kim Morrison]

max said:

I guess my question is why doesn't doc-gen4 then have a way to use verso to emit proof state traces in the static documentation. That is the feature that I wanted to address

This is being actively worked on.