Latexing Lean

Stream: general

[Ashvni Narayanan]

I am writing up a project in Overlead, and I need to put in my Lean code. I have got the lstlean.tex file (https://github.com/leanprover/lean/tree/master/extras/latex), however I continue to get errors.

Any help is appreciated, thank you!

[Johan Commelin]

What kind of errors?

[Ashvni Narayanan]

Package ucs: Unknown Unicode character 65533 = U+FFFD,
(ucs)   possibly declared in uni-255.def.
(ucs)   Type H to see if it is available with options.

Package Listings: Couldn't load requested language.

Package Listings: language lean undefined.

Package utf8x: MalformedUTF-8sequence.

are some of the 1K+ errors (I shifted to VSCode).

[Johan Commelin]

Hmmm, let me check the top of our perfectoid latex file

[Johan Commelin]

\documentclass[10pt, a4paper]{article}
\pdfoutput=1

\usepackage[utf8x]{inputenc}
\usepackage[LGR, T1]{fontenc}
\PrerenderUnicode{ä}
\PrerenderUnicode{é}

\usepackage{amsmath, amsthm, amsfonts, amssymb}
\usepackage{textcomp}
\usepackage{textgreek}
\usepackage{upgreek}
\usepackage{mathrsfs}

\usepackage[english]{babel}

\usepackage{listings}
\def\lstlanguagefiles{lstlean.tex}
\lstset{language=lean}

[Johan Commelin]

@Ashvni Narayanan I hope something like that works

[Utensil Song]

How about try using https://github.com/leanprover-community/lean/tree/master/extras/latex

[Utensil Song]

It's much more up-to-date

[Ashvni Narayanan]

Johan Commelin said:

Hmmm, let me check the top of our perfectoid latex file

This has changed all my code to :

eywordcolorlet            blackz            symbolcolor:=            0,commentcolor--commentcolorcommentcolorzcommentcolorcommentcolor:commentcolorcommentcolorNcommentcolorcommentcolorsymbolcolor:=commentcolorcommentcolor0

[Johan Commelin]

Oops... then maybe try the suggestion by Utensil

[Ashvni Narayanan]

Johan Commelin said:

Oops... then maybe try the suggestion by Utensil

The same thing happens

[Johan Commelin]

Then there's probably some other thing in your preamble that makes LaTeX unhappy

[Jalex Stark]

most of my latex headaches involving trying to import a pair of incompatible packages

[Jalex Stark]

latex is not a very good programming language, so even mildly fancy things are implemented in brittle ways

[Ashvni Narayanan]

It finally worked! I now have only 17 errors to deal with!

Package ucs: Unknown Unicode character 8613 = U+21A5,
(ucs)   possibly declared in uni-33.def.
(ucs)   Type H to see if it is available with options.

There is now only this one error that I don't know how to fix.

[Ashvni Narayanan]

I copied the preamble given in the sample Latex file.

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/search/.22unknown.20unicode.20character.22

[Johan Commelin]

Others have had that problem before (-;

[Johan Commelin]

I think you need to teach LaTeX a new unicode character

[Ashvni Narayanan]

Ah alright, maybe I can figure it out then. Thanks to all for the help! :)

[Utensil Song]

Seems to be missing unicode replacement for ↥, maybe try adding

{↥}{{\color{symbolcolor}\ensuremath{\mapsup}}}1

to https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.tex

(untested)

[Utensil Song]

If this works, then you could have a first PR to Lean :+1:

[Utensil Song]

and maybe ensure and update the sample.tex integrating @Johan Commelin 's suggestions and symbols from here

[Jannis Limperg]

If you have Unicode troubles, it might be worth trying XeLaTeX or LuaLaTeX for proper Unicode support. I've always used these when typesetting Agda (but I haven't tried Lean yet).

[Anne Baanen]

I can confirm that XeLaTeX works fine for TeXing Lean

[Ashvni Narayanan]

Utensil Song said:

Seems to be missing unicode replacement for ↥, maybe try adding

{↥}{{\color{symbolcolor}\ensuremath{\mapsup}}}1

to https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.tex

(untested)

Ok, I'll do it. Thank you!

[Christopher Iliffe Sprague]

Is it possible to export Lean code to latex?

[Johan Commelin]

What kind of export do you have in mind?

[Johan Commelin]

The posts above show how to display lean code in TeX, but if you want some more fancy formatting then I don't think such tools exist atm.

[Johan Commelin]

There are other tools that convert commented Lean code into nicely typeset html pages. See e.g. http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html

[Christopher Iliffe Sprague]

Oh, I see the posts now, and thanks for the link. What I have in mind is a step-by-step proof, like in https://reference.wolfram.com/language/ref/FindEquationalProof.html

[Johan Commelin]

I think the sandwich file showcases something similar in spirit

[Johan Commelin]

In the future alectryon might be usable with lean, that will give even better results

[Christopher Iliffe Sprague]

What is the common practice for translating proofs from Lean to regular math expressions in publications?

[Scott Morrison]

I don't think anyone has actually been doing that. Proofs in Lean are not really intended for consumption anywhere other than in a Lean-aware editor, and there is no human readable "export" format.

[Scott Morrison]

(Excepting #explode, which is at least Mario-readable.)

[Scott Morrison]

The links above, e.g. sandwich.html, are examples were a human has generated a file that can produce both human-readable HTML, and Lean-checkable proofs.

[Scott Morrison]

This is lovely, but also takes effort.

[Christopher Iliffe Sprague]

From what I've gathered from my reading about the Mathematica extension, one can use #explode and have Mathematica interpret it. And, in Mathematica, one can export LaTeX