Getting started with Lean4

Stream: new members

[Yuri de Wit]

Hi All, I am new here, new to Lean, new theorem proving, new to category theory etc, but I find Lean4 (my first real exposure to Lean) really impressive (CIC, strict, focus on speed, great interop story, macros, extensible syntax and a clean & clever syntax, to name a few).

My interest in Lean4 comes from the real possibility of being able to build real apps with it and less so on theorem proving / verification (although being able to leverage that at some time sounds really enticing). I got the impression from one of the videos from Lean Together 2021 that the idea is to turn Lean4 into a general purpose programming language. I know there is work to do and it may take a bit of time, which is fine for my purposes.

So I am trying to get some real exposure to using Lean4 and nothing better than a small project. I saw some Github issues for "help wanted" and it has some ideas of projects although I may need some mileage with Lean4 before trying to work on some of those (or either lots of hand holding). The ideas that caught my attention were issues related to LSP, linters, for instance.

I also have other things that interest me. Some examples: reusable CLI library to standardize the creation of command line apps, a canonical formatting tool a la 'cargo fmt', Javascript compilation target.

If you have any feedback to how to get started with useful TODOs, please let me know.

Thanks!

[Arthur Paulino]

When it comes to general purpose adoption of Lean 4, the first thing that comes to my mind is backend development. So being able to build servers and to talk to databases would be a neat thing to have as well :D

For example, a while ago I was able to make Lean 4 talk to MySQL servers: https://github.com/arthurpaulino/LeanMySQL

Be mindful, however, that Lean 4 will evolve to attend the needs of mathlib4 first

[Yuri de Wit]

Understood re: "Lean 4 will evolve to attend the needs of mathlib4 first". Make sense specially considering Lean's history.

For example, a while ago I was able to make Lean 4 talk to MySQL servers: https://github.com/arthurpaulino/LeanMySQL

This is helpful on how to setup a project, build etc, thanks.

[Arthur Paulino]

That project uses Lean's FFI to have access to MySQL's C API.
Simply calling lake new MyProject will provide a simpler structure for a minimal Lean 4 project that doesn't need the FFI

[Yuri de Wit]

This (Lean repos created after 2019) shows a list of Lean projects, but I guess it includes all versions of Lean. Should there be Lean vs Lean4 since the language is somewhat different?

[Julian Berman]

There's a tag for Lean4 (by language GH generally doesn't differentiate I think). And eventually Lean4 will eat Lean3 the same as 3 ate 2.

[Julian Berman]

https://github.com/topics/lean4

[Julian Berman]

someone wrote a CLI library as well I think

[Julian Berman]

Yeah, here: https://github.com/mhuisi/lean4-cli