How to extract the blueprint tex files locally?

Stream: PrimeNumberTheorem+

[Terence Tao]

I'm having some issues making the blueprint compile, and due to the way the blueprint is integrated into the lean files in this project, I am unable to solve the problem locally, and am resorting to using multiple updates to my PR to trigger the CI to debug the LaTeX issues. This is of course suboptimal (with one technical complication being that the line numbers that are being reported as problematic by the CI refer to the extracted tex file rather than the original lean file, so it is challenging for me to localize the issue). Is there a way to extract the tex files from the blueprint locally?

A side note: one minor annoyance I encountered with the integrated LaTeX/Lean format is that both the latex and lean files are edited in VSCode using the lean conventions, in particular automatically abbreviating LaTeX strings like \alpha into their unicode equivalents. This was quite annoying until I realized I should write the LaTeX side of the blueprint in a separate tex file first.

To be honest I think I prefer the format used elsewhere in which the blueprint is kept in separate files than the lean files, but presumably the issues here are fixable.

[Terence Tao]

OK, there is some weird plasTeX bug that only emerged recently, because some (but not all) \lean tags that did not cause problems in the past are now creating difficulty. I've commented out enough of the \lean tags to make the blueprint compile for now in my PR as a temporary fix, but I haven't figured out the precise cause yet (in large part due to the issues mentioned above).

[Alex Kontorovich]

Hi Terry, sorry to hear that! You should be able to extract the tex files locally by navigating to your main PNT+ directory and running make blueprint in the terminal. That generates all the TeX files.

[Alex Kontorovich]

For things like \alpha, you just have to type the \ twice to cancel out the auto-unicoder. (But if you have copilot on in the background, it will quickly learn whether you're in the "tex" part of the file or "lean" part, and suggest the corresponding text...)

[Alex Kontorovich]

I don't know about the new plasTeX bug; will have to investigate that tomorrow (but it will probably be above my paygrade. Maybe @Ian Jauslin can figure it out?)

[Kevin Buzzard]

Oh are you doing something different to FLT, where we literally have TeX files for the TeX? Is this Alex's version where the TeX is in the lean files? I have been a bit scared to change to this version and the fact that backslash has different behaviour makes me a bit more scared. I can definitely see the advantages of having them in the same place (esp for AI) but looks like there are disadvantages too?

[Ruben Van de Velde]

Yes, this is the case

[Terence Tao]

@Alex Kontorovich Thanks for the suggestion, but unfortunately it turns out the makefile is not particularly compatible with my Windows setup. I think I could figure out some workarounds by installing WSL or something but this may require more time investment than I currently have available.

The PR by the way is here. After some experimentation, I found that the following lean fragments in lcm.lean were now problematic:

\lean{Criterion.prod_p_le_prod_q}\leanok
\lean{Criterion.not_highlyAbundant_1}\leanok\uses{M-def}
\lean{Criterion.not_highlyAbundant_2}\leanok

giving errors such as this:

plasTeX version 3.1
ERROR: An error occurred while building the document object in ./Lcm.tex on
   line 183 ('TeXFragment' object has no attribute 'strip')
Traceback (most recent call last):
  File "/opt/hostedtoolcache/Python/3.9.25/x64/bin/plastex", line 7, in <module>
    sys.exit(plastex())
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/client.py", line 72, in plastex
    main(sys.argv[1:])
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/client.py", line 52, in main
    run(filename, config)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/Compile.py", line 90, in run
    tex = parse(filename, config)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/Compile.py", line 85, in parse
    tex.parse()
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/TeX.py", line 416, in parse
    item.digest(tokens)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/__init__.py", line 929, in digest
    item.digest(tokens)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/Base/LaTeX/Sectioning.py", line 286, in digest
    item.digest(tokens)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/Base/LaTeX/Sectioning.py", line 286, in digest
    item.digest(tokens)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/Base/LaTeX/Sectioning.py", line 286, in digest
    item.digest(tokens)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/__init__.py", line 929, in digest
    item.digest(tokens)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/plasTeX/__init__.py", line 929, in digest
    item.digest(tokens)
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/leanblueprint/Packages/blueprint.py", line 83, in digest
    decls = [dec.strip() for dec in self.attributes['decls']]
  File "/opt/hostedtoolcache/Python/3.9.25/x64/lib/python3.9/site-packages/leanblueprint/Packages/blueprint.py", line 83, in <listcomp>
    decls = [dec.strip() for dec in self.attributes['decls']]
AttributeError: 'TeXFragment' object has no attribute 'strip'
make[1]: *** [Makefile:2: all] Error 1
make[1]: Leaving directory '/home/runner/work/PrimeNumberTheoremAnd/PrimeNumberTheoremAnd/blueprint'
make: *** [Makefile:20: blueprint] Error 2
Error: Process completed with exit code 2.

On the other hand, other \lean tags of a similar nature went through just fine. This perhaps suggests that the issue lies elsewhere, but it is difficult to diagnose on my end what is going on as my only diagnostic tool currently is to update the PR and wait for the CI to report back.

[Alex Kontorovich]

Thanks Terry; I'm not sure what the error message is showing. Do you want me to merge the PR now, or is it still a draft? I could try to recreate the PR locally line by line and see if I can get to the bottom of the issue?

[Terence Tao]

Well, it has certain \lean tags commented out that used to be functional, so while it technically could be merged as is, I think it would be better to somehow diagnose the issue first (especially since I would like to add a lot of further \lean tags later).

[Alex Kontorovich]

Kevin Buzzard said:

Oh are you doing something different to FLT, where we literally have TeX files for the TeX? Is this Alex's version where the TeX is in the lean files? I have been a bit scared to change to this version and the fact that backslash has different behaviour makes me a bit more scared. I can definitely see the advantages of having them in the same place (esp for AI) but looks like there are disadvantages too?

Yes, we're interspersing Lean with TeX, and scraping the TeX at compilation; it certainly takes some getting used to, but I've personally found it very beneficial. My understanding is that @Pietro Monticone will soon have an even better version, which will even automate a lot of the \uses tagging... (Maybe he can say more on that?)

[Kevin Buzzard]

What I don't like about your set-up is that when I'm writing FLT blueprint in tex files I am getting things like immediate feedback on TeX errors -- all the stuff that one would imagine a modern TeX set-up has. Your idea, whilst great for AI, is a step backwards for TeX convenience, it seems to me. In my mind what we want is some claude.md (or whatever setup you're using) file which just says "to see the LaTeX proof of [some random Lean statement] look for \lean{name of the statement} in the blueprint", rather than "write LaTeX in files with a .lean suffix". But because FLT is not really in a position where AI helps right now and won't be for at least the next few months, I am not particularly motivated to experiment with this.

[Pietro Monticone]

I'll take a look at the PNT+ setup as soon as I find the time and eventually open a PR integrating LeanArchitect if you want. LaTeX syntax highlighting is not available, but planned for future development. Not trivial to implement.

CC: @Thomas Zhu.

[Alex Kontorovich]

Kevin Buzzard said:

What I don't like about your set-up is that when I'm writing FLT blueprint in tex files I am getting things like immediate feedback on TeX errors -- all the stuff that one would imagine a modern TeX set-up has. Your idea, whilst great for AI, is a step backwards for TeX convenience, it seems to me. In my mind what we want is some claude.md (or whatever setup you're using) file which just says "to see the LaTeX proof of [some random Lean statement] look for \lean{name of the statement} in the blueprint", rather than "write LaTeX in files with a .lean suffix". But because FLT is not really in a position where AI helps right now and won't be for at least the next few months, I am not particularly motivated to experiment with this.

I'm guessing that this is "merely" an engineering issue; someone should code up a VSCode+TeXShop overlay where you can see both simultaneously. This already exists in emacs, as @Paul Nelson showed me already two years ago; I'll be shocked if it really can't be done in VSCode... (I think it would be very valuable!...)

[Pietro Monticone]

I talked about this with @Marc Huisinga at #ItaLean 2025. It will require quite a bit of work, but it should be fairly doable. Can't promise anything at this point, but I'll definitely take a closer look.

[Pietro Monticone]

Here is the draft PR.

[Emily Riehl]

I'm visiting from the Infinity-Cosmos project to say that we're planning to give the new Lean Architect a try.

One problem we're having is that the original LaTeX blueprint I wrote no longer tracks the formalization that closely. It would be better for newcomers if I went back and updated it but this feels annoying to have to do. Another issue is that lots of our formalizations get PRed to mathlib very quickly so then aren't really in our git repo anymore, but nevertheless make sense to track in the blueprint. My hope is that Lean Architect will help with all of this.

So if you want to know how the beta testing is going, you can ask me in a few weeks.

[Pietro Monticone]

Sure, I'm going to open a PR integrating LeanArchitect there too soon.

[Alex Kontorovich]

Great thanks Pietro! I see that it's a draft, so I'm guessing I shouldn't merge it just yet. Will it be "easy" for me to figure out how to use the new system? Maybe we can hop on a zoom call once it's ready and you can walk me through it? Thanks!!

[Pietro Monticone]

Not ready yet. It should be ready for review relatively soon.

[Pietro Monticone]

A particularly valuable aspect of LeanArchitect, I believe, is that it allows for proper "blueprint debugging". There were many instances in which this proved genuinely helpful.

[Alex Kontorovich]

I wasted several hours yesterday trying to debug @Terence Tao's PR. I'm locally seeing the same issues as he's having, but have no idea why. The code looks fine to me. The TeX scraper is doing exactly what it's supposed to. So I think the issue is with something PlasTeX is doing? Will be great to try out LeanArchitect and see if it can help...

[Terence Tao]

Sorry to waste your time with this also. I think the issue must be lie in some other portion of the PR, which made a lot of changes to a lot of files. In the future I will try to PR often and in particular trigger CI on a regular basis.

I think what I will do on my end is close my PR and try to reconstitute it with a PR with a sequence of incremental updates trying to replicate the original PR until it breaks, this may help diagnose the problem better.

[Pietro Monticone]

@Alex Kontorovich Could you please explain how I should interpret the codebase in StrongPNT.lean?

[Pietro Monticone]

The document contains numerous LaTeX theorem declarations that are annotated with \lean{…} tags but have no corresponding Lean declarations in the repository, despite being referenced as if they were formalised.

For instance, the following theorem is declared:

\begin{theorem}[BorelCaratheodoryDeriv]\label{BorelCaratheodoryDeriv}\lean{BorelCaratheodoryDeriv}
    Let $R,\,M>0$. Let $f$ be analytic on $|z|\leq R$ such that $f(0)=0$ and suppose $\Re f(z)\leq M$ for all $|z|\leq R$. Then for any $0 < r < R$,
    $$|f'(z)|\leq\frac{16MR^2}{(R-r)^3}$$
    for all $|z|\leq r$.
\end{theorem}

However, no Lean theorem named BorelCaratheodoryDeriv exists anywhere in the project repository

[Terence Tao]

@Alex Kontorovich I have successfully made a PR at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/441 that builds properly. In doing so I realized I also had some mismatched \lean{} tags which likely caused some latent issues that got attached to completely irrelevant lines of LaTeX, but hopefully it is all fixed now.

[Alex Kontorovich]

Pietro Monticone said:

The document contains numerous LaTeX theorem declarations that are annotated with \lean{…} tags but have no corresponding Lean declarations in the repository, despite being referenced as if they were formalised.

For instance, the following theorem is declared:

\begin{theorem}[BorelCaratheodoryDeriv]\label{BorelCaratheodoryDeriv}\lean{BorelCaratheodoryDeriv}
    Let $R,\,M>0$. Let $f$ be analytic on $|z|\leq R$ such that $f(0)=0$ and suppose $\Re f(z)\leq M$ for all $|z|\leq R$. Then for any $0 < r < R$,
    $$|f'(z)|\leq\frac{16MR^2}{(R-r)^3}$$
    for all $|z|\leq r$.
\end{theorem}

However, no Lean theorem named BorelCaratheodoryDeriv exists anywhere in the project repository

Whoops, looks like those \lean tags are too early, there's no corresponding lean statement yet. You can just comment those out. Thanks!

[Alex Kontorovich]

Oops, sorry Pietro, I just realized that by merging Terry's PR I may have ruined your work in progress... hope that's not the case (too much)? Should I pause merging other PRs until we've had a chance to try out LeanArchitect?

[Pietro Monticone]

Terence Tao said:

Alex Kontorovich I have successfully made a PR at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/441 that builds properly. In doing so I realized I also had some mismatched \lean{} tags which likely caused some latent issues that got attached to completely irrelevant lines of LaTeX, but hopefully it is all fixed now.

Oh, that will interfere non-trivially with the other PR...

[Pietro Monticone]

Alex Kontorovich said:

Oops, sorry Pietro, I just realized that by merging Terry's PR I may have ruined your work in progress... hope that's not the case (too much)? Should I pause merging other PRs until we've had a chance to try out LeanArchitect?

Yes , please. Could you please revert the last commit and reopen Terence's branch?

[Pietro Monticone]

There are a lot of "blueprint bugs" to fix like those fixed by Terence in his last PR. I think it's better to fix them in order.

[Pietro Monticone]

Opened PR to revert it since it's much easier and more efficient to proceed in this direction (i.e. adding Terence's changes in the new system).

[Pietro Monticone]

I'm also fixing as many unicode-to-LaTeX as possible

[Alex Kontorovich]

Reverted. Thanks Pietro! Pausing any further merging until we try out LeanArchitect

[Pietro Monticone]

Ok, now everything should be fixed...

[Pietro Monticone]

PNT#439 is now ready for review

[Pietro Monticone]

Fix PNT#443. It’s a draft. I’ll finish it later.

[Pietro Monticone]

Ok, PNT#443 is ready to merge.

[Alex Kontorovich]

Great thanks. Will this also fix the broken blueprint link?
image.png

[Pietro Monticone]

Yes yes, it couldn't possibly work because of a path issue

[Alex Kontorovich]

Argh the build failed... Help please?

[Pietro Monticone]

Everything worked apart from the upstreaming_dashboard thing. Let me comment it out for the moment. I'll fix it later.

[Pietro Monticone]

Oh, it expects _includes and I wrote _include...

[Pietro Monticone]

Fixed and pushed

[Pietro Monticone]

@Alex Kontorovich Could you please go to https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/settings/pages, then Deploy from a branch and click on GitHub Actions?

[Pietro Monticone]

Ok, now everything works fine:

• Website https://alexkontorovich.github.io/PrimeNumberTheoremAnd
• Docs https://alexkontorovich.github.io/PrimeNumberTheoremAnd/docs/
• Blueprint website https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint
• Blueprint PDF https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint.pdf

[Alex Kontorovich]

Many thanks for your help!!

[Terence Tao]

So how does one edit the blueprint going forward? Are the individual lean files still the source of ground truth for the blueprint?

[Pietro Monticone]

Yes, they are.

[Terence Tao]

Are the \lean, \leanok, \uses tags still in use? I don't see them in the lean code, instead there are some other vaguely Lean metaprogramming looking fields instead.

[Pietro Monticone]

The \lean{}, \leanok and \uses{} are not necessary since they're all automatically inferred, but can also be manually set if needed.

[Pietro Monticone]

To generate the blueprint you need to run:

# Generate the blueprint to .lake/build/blueprint using `LeanArchitect`
lake build :blueprint
# Build the blueprint using `LeanBlueprint`
leanblueprint pdf
leanblueprint web

[Terence Tao]

Is there any documentation for LeanArchitect? I guess if it is all done via Lean metaprogramming then in principle I can try to figure it out from the Lean IDE support (infoview etc.).

[Pietro Monticone]

The README should be enough https://github.com/hanwenzhu/LeanArchitect

[Ruben Van de Velde]

What's the replacement for \uses before you've formalized the proof?

[Pietro Monticone]

The uses parameter. You can input both the $\LaTeX$ label or the Lean declaration name.

@[blueprint
  "latex-label"             -- The LaTeX label to use for the node (default: Lean name)
  (statement := /-- ... -/) -- The statement of the node in LaTeX
  (hasProof := true)        -- If the node has a proof part (default: true if the node is a theorem)
  (proof := /-- ... -/)     -- The proof of the node in LaTeX (default: the docstrings in proof tactics)
  (uses := [a, "b"])        -- The dependencies of the node, as Lean constants or LaTeX labels (default: inferred)
  (proofUses := [a, "b"])   -- The dependencies of the proof of the node, as Lean constants or LaTeX labels (default: inferred)
  (title := "Title")        -- The title of the node in LaTeX
  (notReady := true)        -- Whether the node is not ready
  (discussion := 123)       -- The discussion issue number of the node
  (latexEnv := "lemma")     -- The LaTeX environment to use for the node (default: "theorem" or "definition")
]

You can also use the tactic sorry_using [decl1, decl2, ...] if you find it convenient.

[Pietro Monticone]

Terence Tao said:

Is there any documentation for LeanArchitect? I guess if it is all done via Lean metaprogramming then in principle I can try to figure it out from the Lean IDE support (infoview etc.).

No metaprogramming is needed. It should be very easy for the user.

[Terence Tao]

How does one create a blueprint entry for a step for which one has not formalized even the statement yet? Does one need to create a stub theorem with a stub type for this?

[Terence Tao]

Regarding my previous PR, should I reconstruct it using the new format, or do you have an automated tool to do this?

[Pietro Monticone]

Terence Tao said:

How does one create a blueprint entry for a step for which one has not formalized even the statement yet? Does one need to create a stub theorem with a stub type for this?

You can create a blueprint_comment in pure LaTeX. See StrongPNT.lean for example.

Alternatively, yes, you can create a stub type.

[Pietro Monticone]

Terence Tao said:

Regarding my previous PR, should I reconstruct it using the new format, or do you have an automated tool to do this?

Unfortunately there is no automated tool for that conversion.

[Terence Tao]

OK then I will work to reconstruct a PR with the new format.

[Pietro Monticone]

If you add new Lean files in your PR (e.g. PrimeNumberTheoremAnd.BKLNW), you need to update the blueprint/src/blueprint.tex accordingly (e.g. \inputleanmodule{PrimeNumberTheoremAnd.BKLNW}).

[Terence Tao]

A single blueprint item can only tag a single lean object, right? In contrast to a vanilla blueprint where one can \lean{} multiple lean functions in a single blueprint theorem.

[Pietro Monticone]

No, multiple Lean declarations may correspond to the same LaTeX in the blueprint, by specifying the same label as:

@[blueprint "thm:a"] theorem a_part_one : ...
@[blueprint "thm:a"] theorem a_part_two : ...

The output will use \lean{a_part_one, a_part_two}, and \leanok only if both a_part_one and a_part_two are sorryless, and the \uses will also be merged.

[Terence Tao]

Ah, ok. So the metadata for "thm:a" such as title or statement only needs to be declared once?

[Terence Tao]

OK, managed to convert the PR over. Github Copilot was very helpful in transferring the format over after showing it the first few examples.

[Pietro Monticone]

Terence Tao said:

Ah, ok. So the metadata for "thm:a" such as title or statement only needs to be declared once?

In the current version, we should still care about ordering of duplicates.

So, for example, in situations like:

@[blueprint
  "fks2-lemma-20"
  (title := "FKS2 Lemma 20")
  (statement := /--
  Assume $x \geq 6.58$. Then $Li(x) - \frac{x}{\log x}$ is strictly increasing and $Li(x) - \frac{x}{\log x} > \frac{x-6.58}{\log^2 x} > 0$.
  -/)]
theorem lemma_20_a : StrictAntiOn (fun x ↦ Li x - x / log x) (Set.Ioi 6.58) := sorry

@[blueprint
  "fks2-lemma-20"]
theorem lemma_20_b {x : ℝ} (hx : x ≥ 6.58) :
  Li x - x / log x > (x - 6.58) / (log x) ^ 2 ∧
  (x - 6.58) / (log x) ^ 2 > 0 :=
  sorry

The second one overwrites the first one in terms how things get displayed after running leanblueprint web, so one should move the metadata to the final appearance of the tag or duplicate the metadata too if you prefers.

To be clear, this is what happens with the code chunk above.

[Pietro Monticone]

Reviewed and merged @Thomas Zhu’s PR bumping LeanArchitect in order to fix a bug and remove this ordering limitation.

[Alastair Irving]

Runs seem to be significantly slower since these changes. It used to take about 5 minutes but now its more like 15. Do we know why this is, have we lost some parallelism in the build?

[Pietro Monticone]

Not all files were in the build file before. We have properly run lake exe mk_all to make sure.

[Pietro Monticone]

And now we have build_args. I don’t think it’s a big issue.

[Ruben Van de Velde]

15 minutes for a normal build or only when you're building the blueprint? Or is there no such distinction anymore?

[Pietro Monticone]

15 minutes for a normal build or only when you're building the blueprint?

When you're building the blueprint.

Or is there no such distinction anymore?

They're happening in the same job step Build the project with :blueprint as build_args provided by the lean-action. They can separated but I don't see any good reason to do it.

[Ruben Van de Velde]

I was wondering mostly about local builds

[Pietro Monticone]

No difference locally. Just run lake build instead of lake build :blueprint.

[Pietro Monticone]

But the difference you get might be mostly due to more files being imported in the build file PrimeNumberTheorem.lean

[Thomas Zhu]

I can actually reproduce the issue that @[blueprint] makes the build (without blueprint) significantly longer locally. I will debug this tonight, hopefully it is not hard to fix. It is probably caused by LeanArchitect interfering with Lean's asynchronous elaboration.

[Pietro Monticone]

Oh, didn't notice that. Thanks!

[Thomas Zhu]

This PR should fix the slowness issue:
https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/447

[Pietro Monticone]

Thank you, Thomas. I will proceed with the merge once the CI checks have completed.

[Pietro Monticone]

Opened PNT#509 to set up statement and proof LaTeX docstrings foldability in VS Code via the Explicit Folding extension.

foldable-doctrings.mp4

[Pietro Monticone]

Oh, I've just noticed that @Terence Tao added sublemma envs which were not correctly displayed because not included by default. Fixed it by adding the thms option to the \usepackage{blueprint} line in web.tex file.

[Pietro Monticone]

I've just noticed that the \discussion URLs were wrong due to how the web.tex had been set up (i.e. missing \github and \home).

Now it should be fixed. It locally works fine. Let's see if it gets deployed correctly...

[Pietro Monticone]

Confirmed. It works correctly now.