Typesetting Lean code on slides

Stream: mathlib4

[Michael Rothgang]

There used to be a page on an old Lean manual about how to typeset Lean code (for presentations), but I cannot find this any more. Anybody have a hint for me?

[Christian Merten]

I use minted and with an up-to-date version it works out of the box. You need to use the fragile option for frames though.

[Eric Wieser]

I've added a beamer example to https://www.overleaf.com/read/cgqkbtvqrsdr#4440c9

[Michael Rothgang]

That also works with beamer?

[Christian Merten]

Yes

[Michael Rothgang]

(I can't view the overleaf project.)

[Eric Wieser]

Fixed

[Eric Wieser]

Of note is that overleaf just got TeXLive 2025, which comes with a recented pygments that understands Lean 4 (edit: but before I fixed some highlighter bugs, a local install of pygments will work better)

[Michael Rothgang]

Thanks! This is really helpful.

[Michael Rothgang]

Let me ask a follow-up question: what's your favourite fix to
LaTeX Error: Unicode character ℝ (U+211D) not set up for use with LaTeX.

[Michael Rothgang]

Using xelatex, I guess?

[Michael Rothgang]

(Except now I'm getting font problems... :see_no_evil: )

[Eric Wieser]

LuaLatex is what that template project uses

[Kenny Lau]

it's 2025 and we still can't use ℝ??

[Eric Wieser]

It's 2025 and people still using pdflatex get what they asked for

[Bhavik Mehta]

I use pdflatex and ℝ works fine for me in beamer!

[Michael Rothgang]

What trick do you use to make it work? I'll happily use pdflatex (or xelatex), at this point I just prefer any solution that works for me.

[Eric Wieser]

Lualatex with juliamono (as in the template) gives you every unicode character you might need (and in the same font as the web editor)

[Eric Wieser]

pdflatex requires you to manually draw every character that isn't in the standard font

[Bhavik Mehta]

Michael Rothgang said:

What trick do you use to make it work? I'll happily use pdflatex (or xelatex), at this point I just prefer any solution that works for me.

I'll be honest: I don't know, ever since I can remember it just worked for me! I need to put fragile on frames that include code, and I have \usepackage[utf8x]{inputenc} and \usepackage[T1]{fontenc} in the preamble, but other than that I think everything is just default usage of lstlean.tex. So that's just https://lean-lang.org/documentation/latex-syntax-highlighting/

[Patrick Massot]

I use Typst for all my new slides and it makes all those problems go away. I understand typing papers in LaTeX because this is what journals ask for, but I don’t see the point of using it for slides.

[Michael Rothgang]

That might indeed be the way to go... it's just the inertia, at this point.

[Michael Rothgang]

(My experience this morning was... painful enough that I'm happy to switch to anything else almost immediately.)

[Patrick Massot]

I’m not saying everything you can do with beamer can easily be done in Typst, but if you don’t do anything fancy and want to show code then it’s much easier in Typst. There is no analogue of [fragile] and to embed code you simply use backticks as you would do on Zulip.

[Eric Wieser]

@Michael Rothgang, I'm guessing you didn't try just duplicating my overleaf project and writing your beamer code there where everything is already set up correctly?

[Michael Rothgang]

I tried running the file (in the overleaf project) locally, and got errors I didn't understand. I could have run beamer on overleaf, but given I had an alternative, gave up for now.

[Eric Wieser]

Right, the overleaf project explicitly states in main.tex that you need all the files in the project _and_ the overleaf settings, not the source alone :)

[Joseph Tooby-Smith]

Somewhat related to this conversation, I am having trouble with overleaf and pasting Lean code. In particular pasting e.g. ℤ works fine, but when pasting 𝓩 (\MCZ in Lean) I get ��. This seems independent of any compiler I use for the LaTeX. (Pasting 𝓩 into my VS code version of latex works fine).

[Johan Commelin]

Sounds like a bug in overleaf

[Joseph Tooby-Smith]

(I found a way around this which was just to replace 𝓩 in my code blocks with \MCZ when pasting them into LaTex and use \usepackage{listings} and an appropriate substitution to take care of the rest)

[Yury G. Kudryashov]

@Eric Wieser Would it be hard to have a github repo with a file that compiles locally (e.g., using latexmk or something like that for settings) as well?

[Eric Wieser]

Johan Commelin said:

Sounds like a bug in overleaf

Yes, this is a bug in overleaf that they inherit from codemirror. I reported this to them over a year ago.

[Eric Wieser]

Amusingly you can push the correct character to overleaf with git, but then the editor refuses to open your tex file.

[Eric Wieser]

Yury G. Kudryashov said:

Eric Wieser Would it be hard to have a github repo with a file that compiles locally (e.g., using latexmk or something like that for settings) as well?

It would probably need to be a container of some kind to manage pygments / TeXLive versions / fonts. I set up such a container on GitPod for my thesis, but of course gitpod is no more.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Joseph Tooby-Smith said:

Somewhat related to this conversation, I am having trouble with overleaf and pasting Lean code. In particular pasting e.g. ℤ works fine, but when pasting 𝓩 (\MCZ in Lean) I get ��. This seems independent of any compiler I use for the LaTeX. (Pasting 𝓩 into my VS code version of latex works fine).

I have found that even when rendered incorrectly in the Overleaf editor, some Unicode characters will still compile to the correct PDF (on Overleaf) if the LaTeX settings support that.