Can Blueprint latex be inline in the Lean files?

Stream: general

[Geoffrey Irving]

I have an upcoming AI safety formalization project where I want to use Blueprint. Which is fun, as I haven’t used it before.

It seems like the standard setup is Blueprint latex files which are separate from the .lean files. What’s the rationale there?

And, depending on that rationale, I’m curious if it’s possible to do inline Blueprint somehow where a single file contains both. This would require either the Latex to be part of the docstrings, or a flipped version where a file that is “toplevel latex” has Lean blocks which can be compiled or interacted with via VSCode.

[Ruben Van de Velde]

See https://github.com/AlexKontorovich/PrimeNumberTheoremAnd?tab=readme-ov-file#use-of-latex-inside-lean

[Geoffrey Irving]

Nice! It would be good if this was mentioned in the Blueprint repo it self: https://github.com/PatrickMassot/leanblueprint

[Kevin Buzzard]

I am very much in two minds about this approach. The pros are that it makes it much easier for a language model to start filling in your proofs for you. The cons are that you lose all the quality-of-life tools which you get when writing LaTeX in a normal LaTeX-aware environment e.g. VS Code + LaTeX workshop extension.

[Geoffrey Irving]

^ It’s a shame one can’t have both! If they’re both VSCode setups, it seems not too far off to have them work together.

[Shreyas Srinivas]

It’s hard to get them both together. One approach that could work is an adaptation of Jupyter notebooks that renders latex in place for latex cells and shows live infoview on lean cells. I think @Utensil Song got a lean kernel working with Jupyter, but I don’t know if it shows the infoview on lean cells inline

[Shreyas Srinivas]

Link: https://github.com/utensil/lean4_jupyter

[Johan Commelin]

A cheap hack might be to have a shell-script that converts back and forth between .lean and .tex files, inverting the set of marked-as-the-other-language lines.

[Kevin Buzzard]

The problem is that I can envisage in practice a lean file looking like tex then lean then tex then lean then..., and if you turn it into a Tex file and then edit it, it might be hard to turn it back into the modified lean file with just a shell script

[Johan Commelin]

Here's a very crude attempt. Consider the following Python script

#!/usr/bin/env python3

import sys
import argparse

def convert_tex_to_lean(input_stream, output_stream):
    in_minted_block = False
    for line in input_stream:
        stripped_line = line.strip()
        if stripped_line.startswith('\\begin{minted}'):
            in_minted_block = True
            output_stream.write('-- </tex>\n')
            continue
        elif stripped_line.startswith('\\end{minted}'):
            in_minted_block = False
            output_stream.write('-- <tex>\n')
            continue

        if in_minted_block:
            output_stream.write(line)
        else:
            output_stream.write(f'-- {line}')

def convert_lean_to_tex(input_stream, output_stream):
    in_tex_block = True
    for line in input_stream:
        stripped_line = line.strip()
        if stripped_line == '-- <tex>':
            in_tex_block = True
            output_stream.write('\\end{minted}\n')
            continue
        elif stripped_line == '-- </tex>':
            output_stream.write('\\begin{minted}{lean}\n')
            in_tex_block = False
            continue

        if in_tex_block:
            output_stream.write(line[3:])  # Remove the '-- ' prefix
        else:
            output_stream.write(line)

if __name__ == "__main__":
    parser = argparse.ArgumentParser(description='Convert between .tex and .lean files.')
    parser.add_argument('direction', choices=['t2l', 'l2t'], help='Direction of conversion')
    args = parser.parse_args()

    if args.direction == 't2l':
        convert_tex_to_lean(sys.stdin, sys.stdout)
    elif args.direction == 'l2t':
        convert_lean_to_tex(sys.stdin, sys.stdout)

then you can run

$ cat tmp/lean-tex-example.tex | ./tmp/lean-tex.py t2l | ./tmp/lean-tex.py l2t
\documentclass{article}
\usepackage{minted}

\begin{document}

\section{Lean Code Example}

Here is an example of a simple Lean function:

\begin{minted}{lean}
def add (a b : Nat) : Nat :=
  a + b
\end{minted}

And here is a proof of a simple theorem:

\begin{minted}{lean}
theorem add_comm (a b : Nat) : a + b = b + a :=
  Nat.add_comm a b
\end{minted}

\end{document}

which performed the identity transformation.

The intermediate Lean file looks like

-- \documentclass{article}
-- \usepackage{minted}
--
-- \begin{document}
--
-- \section{Lean Code Example}
--
-- Here is an example of a simple Lean function:
--
-- </tex>
def add (a b : Nat) : Nat :=
  a + b
-- <tex>
--
-- And here is a proof of a simple theorem:
--
-- </tex>
theorem add_comm (a b : Nat) : a + b = b + a :=
  Nat.add_comm a b
-- <tex>
--
-- \end{document}

[Johan Commelin]

There is certainly room for improvement here... I didn't think hard about it.

[Kevin Buzzard]

But we're talking about applications to blueprints, where there is no \minted, there is \lean{label} and \leanOK etc, and you don't want the Lean code at all in the LaTeX. Maybe the idea is that you comment out the Lean proofs in the LaTeX?

[Johan Commelin]

Yeah, it's easy to swap out the minted for a block of comments.

[Kevin Buzzard]

I guess another issue would be that typically there might be many Lean files associated to one latex file, and even annoying cases like "the arguments in this latex file are mostly in one lean file except that a couple of them in the middle are sufficiently useful that they are in the for_mathlib folder"

[Johan Commelin]

Agreed. Although I think that issue doesn't play a role for projects like PNT+, where they start with Lean files that contain some TeX.

[Eric Wieser]

Is a polyglot document possible?

[Eric Wieser]

That is, have one file and switch between telling your editor whether to treat it as Lean or latex

[Kevin Buzzard]

There would be a certain amount of hackery involved in getting it to compile in both languages but as I say I'm not 100% happy with this kind of solution because I don't see why we want the linearity of the latex document to be forced on the lean code.