Discussion thread - Side by Side blueprint

Stream: ecosystem infrastructure

[Eric Vergo]

Discussion thread for #announce > Side-by-side blueprint - Experience prototype

[Yaël Dillies]

I see you are putting this on a website. Is it possible to instead have this as a vscode extension or in the lean infoview? The one most annoying thing for me is how long it takes to build the blueprint, only to realise you've missed a dependency...

[Alex Kontorovich]

You can serve it locally, where it builds much faster. (That's what I typically do with PNT+ and RealAnalysisGame projects.)

[Yaël Dillies]

Yes, but I couldn't easily do this until recently due to gitpod wiping out any local config when restarting a workspace. Now that I use the uni's big computer, it shouldn't be so much of an issue anymore

[Eric Vergo]

Yaël Dillies said:

I see you are putting this on a website. Is it possible to instead have this as a vscode extension or in the lean infoview? The one most annoying thing for me is how long it takes to build the blueprint, only to realise you've missed a dependency...

Displaying things in the info view seems like a great idea that I had not considered. It's a bit tight on space though, what were you imagining? showing the rendered Latex of he declaration you're in?

I set up some basic caching, although it's still a bit brittle (and dep. graph change triggers a complete rebuild). I will work on it a bit more this evening. Here are the preliminary results. I expect that they won't get much better than this, but there is still a bit of work to do on making sure it doesn't break. (this is from the first and only successful run)

Screenshot 2026-02-05 at 6.46.26 PM.png

Also I thought about doing a VSCode extension, but could not decide on how I wanted to do it. There are a lot of design decisions to be made in terms of where the lean and latex go, and where the rendered content gets displayed. I decided to opt out and just display it via html because that seemed to be pretty popular with the original leanblueprint and I figured people would not want to change workflows that much. In principle there is nothing stoping us from doing both.

[Yaël Dillies]

My idea having it in vscode is simply to avoid switching back and forth many times between vscode and my browser. The infoview ultimately is just displayed html, so you could simply strip down your page slightly (so that it fits on a narrow window, and display it in vscode

[Eric Vergo]

Yaël Dillies said:

My idea having it in vscode is simply to avoid switching back and forth many times between vscode and my browser. The infoview ultimately is just displayed html, so you could simply strip down your page slightly (so that it fits on a narrow window, and display it in vscode

Ok, after playing around with things for a bit I was able to put this together (it's mostly spaghetti code, but it works). The big technical change was moving some of the 'dressing' upstream to allow for things like:

• Latex that is captured in the blueprint attribute is now live rendered in the infoview
• Displaying the colored status indicator dot in the infoview
• Building and serving the side-by-side blueprint in VSCode
• Better cache management

It's still fragile and unoptimized with obvious formatting bugs, which I plan to fix. But before going through the effort of doing that I wanted to share and get people's feedback. Video and beauty shots below; let me know what you think.

Screenshot 2026-02-09 at 9.46.42 AM.png

Screenshot 2026-02-09 at 9.59.56 AM.png

https://www.youtube.com/watch?v=2NbDpH2au3g

[Johan Commelin]

That looks really cool!

[Yaël Dillies]

That looks great! Is it much harder to support blueprints written in tex?

[Yaël Dillies]

Also, I'm unsure what the above and below fields are for

[Eric Vergo]

Thanks for the kind words! I'll address your points while explaining things in a bit more detail.

• "Nodes" contain all of the mathematical content and are tied 1-1 to individual declarations in lean files. This includes the dressed content, which is generated during elab. This is mirrored in the code by having all of the relevant content defined inside the @[blueprint] attribute using options. This is a fundamental change from the original leanblueprint (which used a tex file for everything) and the PNT project, which used leanarchitect to store some content in the attribute, and some at the end of the file using comments with custom delimiters.
• Even though most of the content is now in the attributes, there are still tex files governing the layout as well as a limited amount of content in the blueprint and/or paper. These define things like chapters, titles, sections, as well as what content gets pulled from the node and displayed. There are many different ways to have the user store the lean/latex together, and this is only one of them. I am very open to doing this differently.
• Doing all of this in verso instead of tex is the right long term solution for many reasons, but I wanted to use tex files because. 1) It's the devil I know and allows me to prototype fast 2) It's more flexible and has off the shelf tooling for a lot of things 3) It enables the following: Lets say a mathematician unfamiliar with lean wants to formalize some work of theirs. They can then copy/paste the latex into blueprint attributes one by one, providing a more structured formalization UX. It will never be perfectly smooth of course, but giving newer users something familiar to anchor themselves to may be helpful.
• The above/below fields in the attribute are meant to capture additional expository content that is not directly part of the declaration in lean. This allows for more coherent documents that are more than just a list of declarations. This wouldn't be included in, say, mathlib entries, but it would be useful for people creating pedagogical works. Example.

Screenshot 2026-02-11 at 10.06.55 AM.png

Other random thoughts:

• I'd like to support images/figures/plots. This shouldn't be too hard to make work and I think it could offer a lot to the experience/product
• Alex K. suggested that we make tex a first class citizen in the lean file. To start, I was thinking that we add latex syntax highlighting. If we have the latex in the blueprint attribute we should be able to pass it to a dedicated latex syntax highlighting tool and display it as if it were real tex
• The VSCode extension is a natural fit for the emerging agentic AI ecosystem. Claude Code, VSCode forks like cursor and windsurf, and many other AI tools use VSCode as their main interaction point with humans and code . Should we be designing these tools for use by humans/agentic ai/both?
• Placing all of the relevant mathematical English just above the corresponding lean in the file sets one up very well for auto formalization efforts. We could also have a small, highly dedicated llm that generates lean declarations off blueprint attributes with these options. One could imagine a highly-specialized LLM that only does this task running locally on your machine. Note how the data set that would be used to train this model grows over time, and how we will always have a perfectly clean signal about which generations were correct and which were not. This means that over time you will accumulate an ever-growing data set to train the next iteration of the model on, which gives you a better tool, which then helps you generate more data, ... lather, rinse repeat.

[Yaël Dillies]

I am afraid in practice it isn't really the case that a blueprint item corresponds to a single mean declaration. It's oftentimes one-to-many, or one-to-none