Greetings & Questions

Stream: new members

[Yingte Xu]

Hi everyone. I am a PhD student at the University of Technology Sydney. My major is programming language theory, and I found LEAN may be helpful in my work. After going through the introductions, I still have some questions:

1. What is the status of the mathlib for LEAN4? Are we rewriting it in LEAN4, or are the former libraries simply suited for LEAN4?
2. Things like partially ordered sets or domain theory are essential for program analysis. If there is no existing work on this in LEAN, maybe I can help.

[Calvin Lee]

to answer 1, I would look around the #mathlib4 channel where mathport is discussed. I believe the plan is to port mathlib to lean4, but that effort is not nearly done. Feel free to read the last mathport status report for more context