Zulip Chat Archive

Stream: new members

Topic: Greetings & Questions


Yingte Xu (Jul 29 2022 at 03:35):

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 (Jul 29 2022 at 03:39):

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


Last updated: Dec 20 2023 at 11:08 UTC