28
$\begingroup$

The Natural Number Game suggests the possibility of rewriting mathematics textbooks with embedded interactive Lean code. I'm envisioning something like Google Colab or Mathematica, where you can insert either code blocks or text/LaTeX blocks.

Question: Is there already a good package for doing this?

If there were one, and it were available readily, this would accelerate the interface between mainstream mathematics and proof assistants. (Imagine classic mathematics texts rewritten with embedded code exercises.)

The best so far, to my knowledge, Patrick Massot's formatter discussed here, and maybe this is good enough? I'd be interested in knowing what is being done, and collecting the results here.

(Maybe this is CW?)

Improve this question
$\endgroup$
3
  • 10
    $\begingroup$ There is a Lean mode for the LaTeX listings package that lets you display Lean code in LaTeX documents. But I suppose you're really looking for a Lean literate mode, like literate Agda. I don't think there is one. $\endgroup$
    – Andrej Bauer
    Commented Feb 8, 2022 at 20:16
  • 3
    $\begingroup$ The Natural Number Game was made using Mohammed Pedramfar's Lean Game Maker. $\endgroup$
    – Kevin Buzzard
    Commented Feb 8, 2022 at 22:30
  • $\begingroup$ Thank you both. This is the kind of info I was looking for! $\endgroup$
    – Jon Bannon
    Commented Feb 8, 2022 at 23:19

2 Answers 2

Reset to default
16
$\begingroup$

The tool Alectryon https://github.com/cpitclaudel/alectryon aims to enable writing literate formal proofs, and produces very nice outputs. E.g. https://alectryon-paper.github.io/bench/books/interpreters.html

While it has been developed mostly for the Coq proof assistant, it is in principle not tied to Coq, in fact there is Lean 3 support (https://github.com/cpitclaudel/alectryon#lean-3) and Lean 4 support is being added at https://github.com/insightmind/LeanInk/.

It is not a live workbook-like tool like Mathematica, so writing does involve a compile step to produce a static HTML document. And the code samples are only interactive in the sense that they can be stepped through rather than rewritten in place, so this is not yet a tool for enabling interactive exercises.

Improve this answer
$\endgroup$
11
$\begingroup$

There is also Patrick Massot's https://github.com/PatrickMassot/leanblueprint which is powering

This is not so much a package that formats Lean code into LaTeX, but it is certainly helping to

accelerate the interface between mainstream mathematics and proof assistants.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks! This is awesome. $\endgroup$
    – Jon Bannon
    Commented Apr 16 at 18:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.