On embedding blueprint TeX within Lean

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

We had a small discussion earlier about embedding blueprint TeX right inside Lean, and some weren't so keen on it. But now that we've been doing it for a while in this project, I'd like to record the following. Besides the fact that it greatly helps Copilot to generate Lean from TeX (and vice-versa!), it also makes it 1000 times easier when reorganizing. On quite a few occasions, I've wanted to grab large chunks of code+text and move them around somewhere else in the page, or to another file. Imagine how much more time-consuming/annoying it would be if I had to do this twice, in a coordinated way between two (or four!) separate documents!...

[Yaël Dillies]

Why would you need to do it across separate documents? Are you making the Lean files structure match the blueprint structure?

[Alex Kontorovich]

Yes exactly. (Well, except for really trivial small lemmas.) Isn't that how blueprint is meant to work?...