Can I use Lean 4 without Mathlib4?

Stream: lean4

[Casavaca]

I'm a new comer and I had a question: Can I use Lean 4 without Mathlib4?

I asked because I found that some basic theorems are not in Lean, but in Mathlib.

example 1. min_comm
example 2. Order.lean

Lean has Ord.lean but it doesn't have Preorder, PartialOrder`, etc.

My guess is that Lean 4 can be used without Mathlib4. If so, can I add some theorems to Nat (e.g., min_comm)? Is such contribution welcomed?

[Leonardo de Moura]

@Casavaca Yes, you are correct. Lean 4 can be used without Mathlib 4. Recall that Lean 4 and Lake are implemented in Lean itself, and most of the repos at https://github.com/topics/lean4 do not depend on Mathlib 4.

If so, can I add some theorems to Nat (e.g., min_comm)? Is such contribution welcomed?

I think it is not a good time for this kind of contribution. People are working hard to port Mathlib to Lean 4, and trying to refactor it (e.g., moving stuff to the core repo) while doing the porting will probably create unnecessary headaches.

That being said, after the porting, we want to organize things better and make sure Lean is a great system for mathematicians, computer scientists, and software developers. The mono-repo approach used in Mathlib is working great for formal mathematics, but it is not ideal for people interested in using Lean as a programming language and having basic theorems like the one you mentioned available.

For now, I would suggest you keep this theorem in your own repo if you want to avoid Mathlib 4 as a dependency.