Is there a notebook interface for Lean 4?

Stream: general

[Mr Proof]

I am looking for a notebook interface for Lean 4? If there is not one already, I will make one myself for my own purposes or for others to use. By notebook I mean the kind of thing used by Maple and Mathematica and wxMaxima.

Basically the idea is that there are cells and after typing in a cell like #eval 2+2 in the cell beneath it shows the answer pretty typed in latex

For doing proofs after you type a tactic in an input cell, in the output cell it shows the goals so far. (Unless you type a ; after the input).

You could insert new cells higher up the notebook and then it would re-evaluate all cells below it that depend on this new information.

I think this would make proofs much easier to follow as you could see the goals in order. (Or you could choose to hide all the output cells or hide the input cells.) Currently using the web interface you have to step through the tactics to see the goals in the right hand panel.

This is just for my own purposes as this is how I like to do things. If other people prefer the current method of showing the goals etc. in a different panel then that is also fine too.

[Edward van de Meent]

someone did make this:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lean4_jupyter.3A.20A.20Lean.204.20Jupyter.20kernel.20via.20repl

[Edward van de Meent]

i hope that is what you're looking for

[Edward van de Meent]

another thing you could try is using a local install of lean in combination with vscode rather than the web interface.

[Edward van de Meent]

it's not quite the same thing as you're asking, but i'm certain it will give a better/richer interface than the web interface

[Mr Proof]

Thanks! I will definitely try this out.

[Kyle Miller]

I think this would make proofs much easier to follow as you could see the goals in order.

Maybe for simple proofs with simple goal states. Some parts of mathlib have goal states that look like this (and this isn't even all of it):

image.png

It's worth exploring new interfaces though! Maybe you could show abbreviated goal states by default that only show what's changed, so there are three visibility levels: hidden, terse, and full.

[Kyle Miller]

Some people like the Error Lens extension for VS Code. It adds messages right in the source view:

image.png

[Kyle Miller]

(Speaking of Mathematica, a pipe dream I've had would be an editor interface that uses a "boxes"-like 2D layout system. This isn't to be confused with a structure editor that makes sure everything you write is syntactically well-formed, but instead, rather than strings, the source code is some sort of formatted document, with primitives for superscripts/subscripts, fractions, expandable parentheses, matrices, and so on. We wouldn't need to make so many compromises with mathematical notation if we had this, but it's also a hard sell since there would be no support for it in pre-existing editors or on GitHub!)

[Mr Proof]

Yes, I'd imagine with big goals like that, after you'd broken them down into separate mini-goals, you could hide the original big goal and still have the same information.

On the boxes thing, yes this would be nice. One idea would be to interface with an already built CAS or equation editor and provide some way to translate between lean syntax and a subset of the CAS syntax. Another idea might be to add functions into lean which describe how a lean function like Sqrt is to be formatted in latex or MathML for example. I think these things can be done without altering the underlying lean language.

[Kyle Miller]

By the way, Patrick Massot and I have a library for Lean expressions -> LaTeX (https://github.com/kmill/LeanTeX). Some parts are awkward because Lean notations don't always map cleanly onto math notations.

I'm in the process of rewriting it though for being able to handle hovering over subterms and getting type information. It'd be neat to wire it up to the Infoview at some point.

[Eric Wieser]

Is this a component of your unreleased proof informalization work, or just a project with some overlap?

[Kyle Miller]

Yes, it's a component that was extracted from it.

[Utensil Song]

Hi @Mr Proof , I'm the author of lean4_jupyter, hope you find it useful. Feedbacks welcome!

The current UX is not great for getting the feedback when you are executing the commands/tactics, you'll need to hover the echoed input to see error, warning, and info, that means you are contantly switching between keyboard and mouse/touchpad, some might find it very annoying.

This is inherited from alectryon which is designed to be viewed with focus on the Lean code, and hover to get details, and that detail could be as complicated as Kyle showed in the screenshot, so they can't be expanded by default.

In a next iteration, I hope to figure out a way to solve this, provid a proper feedback without the need to hover, but avoid being too long. The initial idea is to have some heuristics to show all errors, warnings, and the info of the last line by default, and show only the beginning (~ 3 lines?) of a long message.

Also I would like to replace alectryon UI with the Error Lens style (I only know it as squiggle lines before).

[Utensil Song]

B.T.W. There are previous prototypes of Lean 4 kernel that you might want to check out. And the official literate programming way in near future is Verso.

[Mr Proof]

Kyle Miller said:

By the way, Patrick Massot and I have a library for Lean expressions -> LaTeX (https://github.com/kmill/LeanTeX). Some parts are awkward because Lean notations don't always map cleanly onto math notations.

I'm in the process of rewriting it though for being able to handle hovering over subterms and getting type information. It'd be neat to wire it up to the Infoview at some point.

How do you install this for visual studio or the lean web console?