How to be a developer of Lean 4 and what to do next?

Stream: general

[fra guu]

Hi, I want to use lean to formalize some theorems and do some metaprogramming as well. I have recently read some documentation about Lean 4, such as Theorem Proving in Lean, Functional Programming in Lean and Metaprogramming in Lean 4. There's still quite a long way before I can use Lean for development. Could you give me some suggestions about what to do next to ultimately become a developer of Lean 4, like learning from the source code of Lean 4 and mathlib?

[Tomas Skrivan]

I think the best way is to work on a project. Do you have an idea you want to work on? I think you should just start working on it and ask on Zulip whenever you get stuck.

[fra guu]

Tomas Skrivan said:

I think the best way is to work on a project. Do you have an idea you want to work on? I think you should just start working on it and ask on Zulip whenever you get stuck.

Thank you for your suggestion, I will start trying it out.

[Tomas Skrivan]

Do you have any concrete idea right now? I'm curious and people here might be able to point you in the right direction on where to start.

[Floris van Doorn]

This discussion might be interesting to find an interesting project: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.22Missing.20Tactics.22.20list

[fra guu]

Tomas Skrivan said:

Do you have any concrete idea right now? I'm curious and people here might be able to point you in the right direction on where to start.

I want to use Lean's metaprogramming capabilities to implement a programming language, which is mainly used to describe algorithms for a special domain. In other words, algorithms and programs can be written using the defined syntax within Lean files, and the correctness of the algorithms and the proving of related theorems can be achieved through Lean's type system. Perhaps it goes like this: the first step is to define the syntax by 'syntax' and 'macro', and the second step is to define the semantics.

[Shreyas Srinivas]

Never start with the syntax. Start with your desired semantics

[Shreyas Srinivas]

Also, what's your end goal for this? Who are your anticipated end users? Are you familiar with their working style and the kind of language design that will be of use to them?

[Shreyas Srinivas]

Also, when you say algorithms, what sort of a model are you talking about? There are a gazillion of them

[fra guu]

The language is designed for quantum programming to formally verify quantum algorithms and quantum programs. The mathematics used in quantum computation mainly involves linear algebra.

The syntax and some semantics have already been designed preliminarily, and while there are existing quantum programming languages used to run real quantum programs, they are not convenient for formal verification.

The next step is to consider the semantics in detail and how to implement them in Lean. Therefore, I want to learn more about the mechanics of Lean and find some relevant projects.

[Shreyas Srinivas]

The basics of lean can be learnt from the functional programming in lean, and metaprogramming in lean books. As for the rest you'd have to ask an expert on at least one of PL design or quantum algorithms.

[Chris Henson]

@fra guu If you've not seen it already, inQWIRE is a pretty mature collection of Coq libraries for quantum computing. Verification of circuits, optimizations, IR, etc.