LeanTeX - LaTeX presentations from Lean

Stream: general

[Kiran]

Hi Leak Folks, Pleased to announce the release of a library I've been working on for a DSL to construct LaTeX beamer presentations from Lean.

available at: https://github.com/kiranandcode/LeanTeX

LeanTeX - LaTeX presentations in Lean 4

Want to make cool presentations in LaTeX? Want macros and
extensibility without having to learn TeX?

Presenting:

Usage

LeanTeX is made as easy as possible to use!

Create a new Lean project requiring LeanTeX in your lakefile:

-- lakefile.lean
package MyPresentation
-- This is your presentation root
lean_lib MyPresentation where
-- Require LeanTex!
require LeanTeX from git "https://github.com/kiranandcode/leantex" @ "main"

In your Lean project, you can import LeanTeX use its DSL to write LaTex directly from Lean:

-- MyPresentation.lean
import LeanTeX

#usepackage bera
#usepackage hyper

#latex_slide do
     latex![| \titlepage |]

Finally, to build the presentation, run lake exec GenerateSlides:

$ lake exec GenerateSlides
...

Output written on slides.pdf (5 pages, 33772 bytes).
Transcript written on slides.log.

The resulting presentation PDF will be placed in build/slides.pdf

Features

• Escape hatch - latex![| |] acts as an escape hatch for inserting
  arbitrary text into the generated file.
  lean latex![| \author{[|fontsize (size:=18) "Kiran (She/Her)" |]} |]

  The macro itself is an interpolated string, but unlike Lean's
  default string interpolation, we use [| |] to break out back into
  Lean. @{} also is allowed to escape back into Lean.

• DSL for Slides - LeanTex comes with a built in DSL for simplifying
  some LaTeX constructions within Lean:
  slide "Example Slide" do \begin{itemize} \item{"Writing LaTeX-like code within Lean"} \item{"Looks like LaTeX"} \item{"is actually Lean~"} \end{itemize}

• Animations - the with steps macro allows named steps for your
  animations, avoiding the issue with hard to grasp numeric animation indices

  with steps [step1, step2, step3, step4] do
     latex![|
       \begin{tikzpicture}
          \draw<@{step1}->  (0,0) rectangle ++(1,1);
          \draw<@{step2}->  (1,0) rectangle ++(1,1);
          \draw<@{step3}->  (2,0) rectangle ++(1,1);
          \draw<@{step4}->  (3,0) rectangle ++(1,1);
       \end{tikzpicture}
     |]

• Static files - If you create a directory static you can place
  files that should be copied into the build directory

See example for an example of a LeanTeX project.

My personal job talk is also constructed using LeanTeX: https://github.com/kiranandcode/job-talk

[Patrick Massot]

It’s a cool project but the name clash with https://github.com/kmill/LeanTeX is a bit unfortunate.

[Kiran]

ah yes yes I sadly made this in a vacuum and it was only when I came to publish it I realised the name was already in use

I suppose I can probably change my packages' name to LeanBeamer or something, though for now I'm the only user so it's a low priority task

[Yaël Dillies]

Are you aware of @Anand Rao Tadipatri's lean-slides ? It is seems very related to your project

[Yaël Dillies]

Also your github username is currently indicated as gopiandcode on your Zulip profile, which doesn't seem to exist on github. Maybe you typoed?

[Kiran]

ah, thanks for the pointer, I'd neglected to update it on my profile! My github username is kiranandcode!

[Kiran]

Yaël Dillies said:

Are you aware of Anand Rao Tadipatri's lean-slides ? It is seems very related to your project

Ah, yes, I think I had stumbled upon that before. It's a very useful project, though I believe it's targeted more at quick off the shelf presentations, than more custom professional designs suited for, for example, a job talk.

For example, the following slide from my own is built using LeanTex:
Screenshot 2025-08-11 at 9.53.17 AM.png

[Anand Rao Tadipatri]

I agree, LeanSlides was meant more for quick presentations that can be generated entirely from Markdown text, and has limited customisability of style and layout. I think the kind of deep embedding of syntax that LeanTeX provides is fantastic!