Mathlib name. Just checking the meaning(s)

Stream: new members

[Eric Taucher]

On the StackExchange site there is a need for tags for Mathlib. My understanding is that for Lean 3 there is Mathlib and for Lean 4 there is Mathlib 4. Is this correct? Also there are no other things that could be confused with mathlib or would such tags need Lean with them, e.g. lean-mathlib?

[Kyle Miller]

Not answering the question, but in the wild when I mention mathlib, I tend to write lean/mathlib, to recognize there are two parts coming together (so a sort of Stallman-like approach, where he writes GNU/Linux).

I do this mainly to help people who only have heard about Lean to know to search for mathlib, too.

[Anne Baanen]

At the moment there is a mathlib 4, but I'd describe that more as the future version of mathlib being developed in a separate repository instead of an independent project. The expectation is that the whole community will switch eventually.

I don't expect mathlib by itself will be confusing in the context of the Proof Assistant site. Although the name mathlib is generic enough that lean-mathlib is also fine for me. A quick search shows:

• http://mathlib.readthedocs.io/
• https://www.ti.com/tool/MATHLIB
• http://mathlibs.org/
• https://www.ibm.com/docs/en/rbd/9.5.1?topic=variables-egl-library-mathlib
• https://www.nuget.org/packages/MathLib

[Anne Baanen]

Kyle Miller said:

I tend to write lean/mathlib, to recognize there are two parts coming together (so a sort of Stallman-like approach, where he writes GNU/Linux).

I'd like to interject for a moment...

[Jason Rute]

I see this with a lot of proof assistants. metamath is a completely generic logic-agnostic proof assistant, but metamath/set.mm is based on ZFC. I guess Isabelle already goes by Isabelle/HOL but most people probably mean Isabelle/HOL/AFP. I don't know about Coq though... When people say Lean vs Coq, they usually mean Lean/mathlib vs Coq, but I guess that is the point since Coq has many libraries.

[Eric Taucher]

For those interested in tags on the StackExchange site. The associated meta question about mathlib tag names is here.

[Alex J. Best]

Does AFP contain a lot of user-contributed tactics though? I often find it hard to use lean without mathlib because there are just so many tactics, automation and linters that are very useful that you can only get by adding a mathlib dependency, even if I want to write something that doesn't involve mathematics at all!
In that sense it seems Lean and mathlib might be a bit more closely tied than just a proof assistant and a mathemtics library for it.

[Kevin Buzzard]

Furthermore I would imagine that disassociating the tactics from the maths would be very hard work. Tactics like nlinarith will no doubt use a lot of stuff in the earlier parts of mathlib.

[Kevin Buzzard]

I wonder to what extent the fact that lean is written in lean has made our lives easier here. I think the Coq community doesn't have this luxury.

[Karl Palmskog]

Kevin Buzzard said:

I wonder to what extent the fact that lean is written in lean has made our lives easier here. I think the Coq community doesn't have this luxury.

Coq users can metaprogram in Coq itself and thus write tactics/plugins/extensions in Coq, via MetaCoq: https://github.com/MetaCoq/metacoq

[Karl Palmskog]

also, on the topic of Coq vs. its libraries. Coq now has a fully working -noinit option that avoids loading any part of the Coq standard library at startup. This is used most prominently by the Coq-HoTT library, but other libraries such as MathComp are also usable in this way (though not officially like Coq-HoTT).

[Eric Taucher]

I created the tag lean-mathlib

[Eric Taucher]

Only time will tell if this is the wrong way or the right way to name it.