would mathlib users need to learn type theory at some point?

Stream: Lean for teaching

[Bulhwi Cha]

Would Mathlib users have to learn more about type theory at some point? For example, would a math student who uses Lean and Mathlib daily have to know strict positivity at some point?

[Michael Rothgang]

I use Lean and mathlib daily, and I don't know about strict positivity (in the sense of this page). Thus, I think the answer is a strong no, you don't need to know this.

[Bulhwi Cha]

From https://lean-lang.org/theorem_proving_in_lean4/Inductive-Types/#inductive-types:

We will see below that the arguments of the constructors can include objects of type Foo, subject to a certain “positivity” constraint, which guarantees that elements of Foo are built from the bottom up. Roughly speaking, each ... can be any arrow type constructed from Foo and previously defined types, in which Foo appears, if at all, only as the “target” of the dependent arrow type.

[Michael Rothgang]

More knowledge can always be helpful, but you can have very good working knowledge of Lean without a serious background in type theory.

[Junyan Xu]

You need some understanding of positivity to fix your inductive definition when Lean rejects it: #combinatorial-games > Loopy games @ 💬 see also #new members > Definition of an inductive type @ 💬

[Bulhwi Cha]

Michael Rothgang said:

More knowledge can always be helpful, but you can have very good working knowledge of Lean without a serious background in type theory.

I see. Then, do you think there's little chance that a Mathlib user who hasn't learned type theory will mistakenly attempt to define an inductive type in a way that violates Lean's requirements, such as positivity?

[Michael Rothgang]

Sure, when a user runs into this, it is a good time to learn about it. But I personally believe that learning all the theory first is not required. Having access to people who can help them when they get stuck is much more important.

[Michael Rothgang]

(This is my personal opinion, of course. Others may prefer to study Theorem Proving in Lean forwards and backwards before attempting any formalisation on their own. If that works for them, great. But I don't think it's the best strategy for everyone.)

[Bulhwi Cha]

Michael Rothgang said:

If that works for them, great. But I don't think it's the best strategy for everyone.

How much type theory does a mathematician using Lean and Mathlib need to know? I'm pretty sure most Korean students majoring in mathematics haven't heard of types in the sense of type theory. They'd have to learn some basic concepts in type theory to use Lean and Mathlib.

What exactly are those basic concepts? Are lambda terms, currying, Curry–Howard correspondence, dependent types, inductive types, and recursors part of them?

[Michael Rothgang]

You need some working knowledge of Lean, not necessarily a deep theoretical understanding.

[Michael Rothgang]

The details depend on what kind of mathematics you want to formalise. Dependent types are absolutely necessary if you want to formalise e.g. differential geometry, algebraic geometry (and category theory, I hear). I'm not sure if you strictly need them for general topology, for instance.

[Michael Rothgang]

You need to know induction principles, but I'm not sure if you need to know about inductive types (or recursors) to work with them. (You do need them for programming in Lean, of course, but "an inductive type is like an enumeration, except that the variants can carry data, and each variant of a different type" went a long way for me.)

[Michael Rothgang]

lambda terms, currying and Curry-Howard correspondence: all of these are cool knowledge, but I don't think they're required to work with Lean.

[Michael Rothgang]

You can take a look at the Lean courses of e.g. @Kevin Buzzard https://github.com/ImperialCollegeLondon/formalising-mathematics-2024 or @Floris van Doorn https://github.com/fpvandoorn/LeanCourse24/ to see how they teach Lean to mathematicians. Both are experienced Lean users and good teachers.

[Bulhwi Cha]

From https://github.com/ImperialCollegeLondon/formalising-mathematics-2024/blob/c4cfdc64d59c12e07e0c88d702bfe654d518c0bd/FormalisingMathematics2024/Section01logic/Sheet1.lean#L28-L34:

The absolute basics

P : Prop means that P is a true-false statement. h : P means that h is a proof that P is true. You can also regard h as the hypothesis that P is true; logically these are the same. Stuff above the ⊢ symbol is your assumptions. The statement to the right of it is the goal. Your job is to prove the goal from the assumptions.

[Bulhwi Cha]

I guess you can avoid mentioning the propositions-as-types paradigm this way.

[Bulhwi Cha]

Hmm. Most people focusing on mathematics would prefer Kevin Buzzard's approach to teaching mathematics using Lean. It wasn't my cup of tea because it made me feel like I don't know exactly what I'm doing whenever I use Lean's tactics, even though I managed to finish the Natural Number Game four years ago.

[Bulhwi Cha]

By the way, do these courses provided by Kevin Buzzard and Floris van Doorn teach how to define mathematical concepts in Lean and Mathlib?

[suhr]

Bulhwi Cha said:

For example, would a math student who uses Lean and Mathlib daily have to know strict positivity at some point?

Strict positivity is a rather exotic part of type theory. You rarely hit this problem accidentally.

Bulhwi Cha said:

It wasn't my cup of tea because it made me feel like I don't know exactly what I'm doing whenever I use Lean's tactics, even though I managed to finish the Natural Number Game four years ago.

That was my experience as well.

[suhr]

Bulhwi Cha said:

How much type theory does a mathematician using Lean and Mathlib need to know?

There's not that much type theory to learn in the first place. At it's core, Lean is rather simple. But many tutorials fail to communicate this and instead try to hide what's inside like it's something scary.