Lean syntax simplifier

Stream: lean4

[Eric Vergo]

Hey all,

I have been learning lean and continually find myself struggling with reading lean proofs. The syntax comes with a lot of baggage because it was never designed specifically for math, and that makes the learning curve really steep. Rather than complain about it I hacked together a  prototype VSCode extension that defines a custom language and live-translates it to a lean file. Beyond syntax highlighting updates there are a few other things that might help with readability. Here is a quick list of features shown off in the video:

1. Breaks a proof block up into 4 collapsible sub-blocks
2. Allows the user to not define the name for a hypothesis and call it directly in the proof block
3. Grants more freedom for the syntax used in declarations, such as allowing comma separated variable names
4. Allows the user to write ‘via’ in stead of := by” and adds syntax highlighting

I was writing this for myself, but @Alex Kontorovich thought others might be interested. Are there other features you’d like to see? What don’t you like? Any and all feedback is appreciated.

Screen-Recording-2024-09-23-at-10.26.56PM.mov

[Kyle Miller]

You might like looking at @Patrick Massot's Verbose Lean. (Examples)

This language is implemented from within Lean, so it works from within the standard VS Code extension, and it inherits hoverability and all that. It doesn't have any of the collapsibility you have though.

[Eric Wieser]

Are you aware of the rw [‹a + b = 1›] syntax for 2?

[Patrick Massot]

@Eric Vergo This is all nice but indeed you made it a lot more complicated than needed by not using the flexibility of Lean 4 syntax.

[Patrick Massot]

See https://raw.githubusercontent.com/PatrickMassot/verbose-lean4/refs/heads/master/itp2024_paper.pdf for more about Verbose Lean.

[Eric Vergo]

All of your points are well taken, but I think I did a poor job of communicating what I shared this:

Is this partially redundant? Yes. Overcomplicated? Also yes. But I’m not interested in these things right now - this is a hacked together prototype and we can ‘do it right’/optimize it later. Plus I’ve never written anything in Lean before, and have experience with javascript and typescript. So why did I put this together?

For a lot of different reasons, I want all mathematicians to use Lean. And with all due respect to the people who have built it, I don’t think that’s going to happen with the language in its current form. When showing Lean to my professors and other students I have been met with responses such as “gross” and “this looks awful”. Right now asking someone to read a Lean proof is like asking them to read a TeX document rather than the pdf it generates. This is going to significantly reduce the adoption rate, both in terms of speed and overall proliferation. I think we can do better.

In my opinion Verbose lean is clearly better than the default language, but I think this space is worth exploring more. In the interest of that:

Do people see anything with value here? If so I can expand those features.
Do people have any features they know they would love to have? If so I can try to prototype them.
Do people have any ‘pain points’ in the syntax, but don’t know how it could be done better? If so we can brainstorm solutions.

[Kim Morrison]

@Eric Vergo, I think we're all in furious agreement that Lean needs to made easier to read!

My concern with what you're trying to do is that it seems like an all-or-nothing thing: I don't think you're going to get any meaningful adoption unless it can cope with the full variety of Lean syntax as it appears in libraries, and that seems very unlikely for an interface written outside of Lean. (And I'd be skeptical of an argument like "this could be used for custom small libraries for teaching", as that would be doing students a disservice when they had to switch to "standard" Lean.)

Of course I'd be delighted to be proved wrong. :-)

The need to cope with Lean-as-it-is is why I would recommend that to make progress on this front, the right approach is to learn how to make usability improvements that could be deployed for all Lean users (i.e. that use the InfoView, or improve pretty printing, etc. etc.)

[Johan Commelin]

@Eric Vergo One other take on this (and @Patrick Massot has also worked on this together with @Kyle Miller in their informalization project) is the following:

People look at Lean and say "ouch I don't want to read this", and "it is like reading TeX instead of the generated PDF".
But mathematicians don't have any problem with writing TeX. And many of them even define their own macros and packages etc...
But then we still read the beautiful PDFs instead of the raw TeX.

So one way I look at this is: we want a very powerful input language. And it might have a quirky syntax in order to support many powerful features (like macros, metaprogramming, syntax extensions, etc).
But then nothing should stop us from rendering this in a way that is meant for reading instead of writing.

The informalization project by Patrick and Kyle is one prototype for this. And Verso by @David Thrane Christiansen is another project (still WIP) that does this.

Tl;dr: The language we write and the language we read don't need to be identical.

[Johan Commelin]

@Eric Vergo Also: I think it is really good that you are exploring this space! So please don't read my message as "stop doing what you're doing"

[Daniel Weber]

Is there work on delaboration to LaTeX?

[Patrick Massot]

Yes, that part is even public: https://github.com/kmill/LeanTeX

[Eric Vergo]

I didn’t take your message, or anyone else’s for that matter, to mean ‘stop working on this’. This is something I’m interested in, partially aligns with my skillset, and is a place I think I can provide value; so I’m going to continue to tinker. Beyond that I think it’ll help if I share where I’m coming from:

I think Lean is in its relative infancy. To put a fine-point on it, I’m expecting that Lean/mathLib are going to grow by many orders of magnitude in size over the next decade. In my experience the right time to go wide by experimenting is before you go tall and do something millions of times.

We come from very different backgrounds, but I suspect we are here for the same reason: I’m here to build something great, and get the sense that all of you are too.

Screenshot 2024-09-25 at 11.49.20AM.png

[Dan Velleman]

One of my goals in How To Prove It with Lean was to write proofs that are more readable. To some extent this suffers from the problem Kim identified: I wrote some simple tactics to create a "dialect" of Lean that is somewhat different from standard Lean. But the differences are not huge, and I find the proofs easier to read than most Lean proofs.

[Jon Eugster]

another idea where this kind of skill-set could be useful: You know how in VSCode one can open a preview (rendered version) of any .md file by pressing Ctrl+Shift+V? I would love the same feature for a random Lean file, opening a "prettier version" in a new VScode tab as preview, even if "prettier" is something very rudimentary for now which can later be replaced with a better renderer.

[Jon Eugster]

Eric Vergo said:

When showing Lean to my professors and other students I have been met with responses such as “gross” and “this looks awful”.

For what it's worth, I'm still quite amazed about how beautiful Lean as a Language is, while being as expressive as it is! In my opinion it's way better than latex source code! But you are certainly right about certain ideas how to display things.

[Jon Eugster]

In the display for the natural number game we also did this distinction between "declarations" and "assumptions", but I don't think this works as input modus: There are statements which cannot be expressed by having all "declarations" first and then all "assumptions" afterwards.

[Eric Vergo]

Dan Velleman said:

One of my goals in How To Prove It with Lean was to write proofs that are more readable. To some extent this suffers from the problem Kim identified: I wrote some simple tactics to create a "dialect" of Lean that is somewhat different from standard Lean. But the differences are not huge, and I find the proofs easier to read than most Lean proofs.

this looks great, going to check it out.

[Eric Vergo]

Jon Eugster said:

another idea where this kind of skill-set could be useful: You know how in VSCode one can open a preview (rendered version) of any .md file by pressing Ctrl+Shift+V? I would love the same feature for a random Lean file, opening a "prettier version" in a new VScode tab as preview, even if "prettier" is something very rudimentary for now which can later be replaced with a better renderer.

I love this and will find time to put a prototype together. As an exercise I’m going to try and come up with as many other ideas in this space as I can and prototype them. Additionally, I’m planning on doing an independent study under Alex Ryba next semester. We wanted to do something Lean related, but didn’t have a good idea of what to do. Maybe something will come out of this exercise thats worth spending more time on. After hearing your suggestion, if that happens I bet it’ll be something close to what you described, but who knows.

[Eric Vergo]

Jon Eugster said:

Eric Vergo said:

When showing Lean to my professors and other students I have been met with responses such as “gross” and “this looks awful”.

For what it's worth, I'm still quite amazed about how beautiful Lean as a Language is, while being as expressive as it is! In my opinion it's way better than latex source code! But you are certainly right about certain ideas how to display things.

I’m still amazed at the fact anything like this could exist at all. That's why I keep trying to share it with people!

[Eric Vergo]

Jon Eugster said:

In the display for the natural number game we also did this distinction between "declarations" and "assumptions", but I don't think this works as input modus: There are statements which cannot be expressed by having all "declarations" first and then all "assumptions" afterwards.

I don’t think it can work in all situations, but I also think that it doesn’t have to. Maybe the right way to classify what I shared is a ‘notation convention’. This wasn’t shown, but the translator passes anything it doesn’t see in its ‘phrase book’ unchanged. As an example, you don’t have to write ‘via’ in place of ‘:= by’ but you can if you want to.
The example I shared is pretty simple, and that was done so I could focus on getting the code working. I think it makes sense to move on to more complicated files. I was thinking of taking a few proofs from the book as test cases.