Mathlib as a source of definitions

Stream: mathlib4

[Timothy Chow]

It's probably important to draw a distinction between (A) having several different definitions that are provably equivalent, and (B) having several different definitions that are (provably) not equivalent.

Case (A) certainly makes sense in many mathematical contexts. Case (B) is potentially worrisome since it could lead to subtle errors. Thomas Lam has conducted an entertaining survey of mathematical conventions. To pick just one example (number 33), how should one normalize the Fourier transform? There is certainly something appealing about making a particular choice and having everyone stick to it.

On the other hand, I can also imagine that using mathlib as the ultimate arbiter could have unforeseen and undesirable consequences, e.g., if some weird idiosyncrasy of Lean forces itself upon us in an awkward manner. In actual mathematical practice, mathematical definitions live in some kind of "foundation-independent" conceptual space, and insisting too pedantically that a mathematical concept is its definition in some particular foundational system can sometimes have annoying logical consequences.

In John Conway's book, On Numbers and Games, he briefly articulated a manifesto that he called a "Mathematicians' Liberation Movement" (quoted here for example). The manifesto was necessarily somewhat vague, because it was in essence a call to avoid tying oneself too tightly to any particular axiomatic framework.

Again, none of this should be construed as denying that in many cases, it would be useful for there to be a universal definition that everyone agrees to. I'm just cautioning against pushing such an ideology too far.

[Alex Meiburg]

Timothy Chow said:

Case (B) is potentially worrisome since it could lead to subtle errors.

Three terms I'm aware of with lots and lots of different inequivalent, but spiritually connected, meanings: graphs, trees, polygons.

The situation with graphs is the least bad because at least people usually have adjectives they can apply to distinguish what they mean when they want to. "Simple graph", "Finite graph", "Locally finite graph", etc. The situation with 'tree' and 'polygon' is much worse.

[Eric Vergo]

I'm guessing this topic has been discussed at length before the advent of LLMs, and it's not clear to me how 'AI' meaningfully changes the discussion. My understanding is that, at least in theory, these concerns are directly addressable through careful curation of Mathlib, along with the power of dependent type theory + metaprogramming and higher order logic.

To ask a precise question: Is there anything mathematicians do with natural language definitions/proofs that fundamentally cannot be expressed in lean given sufficient effort? I believe the answer is no, but there might be some weird edge cases I am unaware of.

[Kevin Buzzard]

I don't think I've ever done anything in any of my papers which can't be expressed in Lean given sufficient effort, if that's any help. That's why I'm such a believer in the software.

[Eric Vergo]

That's why I'm here too. I want to be able to say anything I want to and be confident of correctness.

[Timothy Chow]

I think there's a subtle distinction that needs to be made. One can ask, "Can every mathematical conjecture/theorem/proof be formalized?" The standard answer to this question is yes. However, a subtly different question is, "Do formalizations of mathematical discourse fully capture everything mathematicians mean by that discourse?" The answer to this latter question is much less clear.

Take some mathematical object such as a group. The concept of a group can be formalized in Lean. But that's not the only option. You can formalize the concept of a group in set theory, or in simple type theory, and each of these options comes in many different flavors. So when mathematicians use the word "group" in natural language, what exactly does it mean? One intuitively wants to say that all the formalizations are equally valid, but if we're being pedantic about it, a formalization of "group" in some dependent type theory is not identical to its formalization in, say, ZFC. So it seems that to properly capture the natural-language meaning of the word "group," we have to say that it's something that transcends any particular formalization. We want to say that the different formalizations are "equivalent" in some sense, but precisely in what sense? It seems we have to introduce some metatheory in which we prove the equivalence, but which metatheory do we choose? Again, we have multiple options. Is it turtles all the way down?

So again, when you ask if something can be "expressed in Lean," it depends on exactly what you mean by "expressed." "Expressing" means drawing some kind of correspondence between formal language and informal language, and so there's no way that we can formally settle whether some formalism "correctly expresses" the informal concept it's supposed to be expressing. This point is related to Kevin Buzzard's point that writing down formal definitions is not something that can be completely automated (until the day that humans stop doing mathematics altogether).

In the normal course of affairs, these nuances aren't that big a deal, because there's usually no substantive controversy about whether some particular formalization of a concept correctly captures what was intended. But for a real-world example, Sergei Artemov has argued that the standard ways of formalizing the notions of "provability" and "consistency" do not correctly capture what Hilbert had in mind. In particular, Artemov produces a PA-proof of the consistency of PA, which you might have thought Goedel's 2nd incompleteness theorem long ago ruled out. But it all hinges on the question of whether the standard formalization of the concept of "consistency" correctly expresses the intended concept.

[Kevin Buzzard]

Whyever would I care about capturing different nuances of the underlying wiring behind groups in various foundational systems? Sylow's theorems don't care about this wiring. You may as well say that a formalisation doesn't capture the fact that group takes 5 letters to spell in English and six in French.

[Yan Yablonovskiy 🇺🇦]

Timothy Chow said:

I think there's a subtle distinction that needs to be made. One can ask, "Can every mathematical conjecture/theorem/proof be formalized?" The standard answer to this question is yes. However, a subtly different question is, "Do formalizations of mathematical discourse fully capture everything mathematicians mean by that discourse?" The answer to this latter question is much less clear.

Take some mathematical object such as a group. The concept of a group can be formalized in Lean. But that's not the only option. You can formalize the concept of a group in set theory, or in simple type theory, and each of these options comes in many different flavors. So when mathematicians use the word "group" in natural language, what exactly does it mean? One intuitively wants to say that all the formalizations are equally valid, but if we're being pedantic about it, a formalization of "group" in some dependent type theory is not identical to its formalization in, say, ZFC. So it seems that to properly capture the natural-language meaning of the word "group," we have to say that it's something that transcends any particular formalization. We want to say that the different formalizations are "equivalent" in some sense, but precisely in what sense? It seems we have to introduce some metatheory in which we prove the equivalence, but which metatheory do we choose? Again, we have multiple options. Is it turtles all the way down?

So again, when you ask if something can be "expressed in Lean," it depends on exactly what you mean by "expressed." "Expressing" means drawing some kind of correspondence between formal language and informal language, and so there's no way that we can formally settle whether some formalism "correctly expresses" the informal concept it's supposed to be expressing. This point is related to Kevin Buzzard's point that writing down formal definitions is not something that can be completely automated (until the day that humans stop doing mathematics altogether).

In the normal course of affairs, these nuances aren't that big a deal, because there's usually no substantive controversy about whether some particular formalization of a concept correctly captures what was intended. But for a real-world example, Sergei Artemov has argued that the standard ways of formalizing the notions of "provability" and "consistency" do not correctly capture what Hilbert had in mind. In particular, Artemov produces a PA-proof of the consistency of PA, which you might have thought Goedel's 2nd incompleteness theorem long ago ruled out. But it all hinges on the question of whether the standard formalization of the concept of "consistency" correctly expresses the intended concept.

This reminds me a lot of this https://philsci-archive.pitt.edu/24324/1/Epistemic_Value_of_Proof.pdf critique of the 'Standard View' .

[Kim Morrison]

Kevin Buzzard said:

I don't think I've ever done anything in any of my papers which can't be expressed in Lean given sufficient effort, if that's any help. That's why I'm such a believer in the software.

Really? You never said that we ought to be able to do something? Hope to do something? Asserted that a technique enables dealing with many similar problems without actually specifying how it should be adapted to each of them. I think many things happen in papers that can't (maybe "should not"?) be formalized.

[Timothy Chow]

Kevin Buzzard said:

Whyever would I care about capturing different nuances of the underlying wiring behind groups in various foundational systems? Sylow's theorems don't care about this wiring. You may as well say that a formalisation doesn't capture the fact that group takes 5 letters to spell in English and six in French.

I think you're actually agreeing with me, perhaps without realizing it. A formalization in Lean forces you to care about the wiring, and therefore fails to perfectly reflect the formalization-independent concept that mathematicians actually have in mind.

[Timothy Chow]

When we say that every mathematically precise statement S can be formalized, what we're really saying is something like, there exists a formal counterpart S' of S in some formal system F with the property that, given any correct mathematical proof (or disproof) of S, we can mimic it in F to yield a formal proof (or disproof) of S'. (I've elaborated on this point before on MathOverflow.) That's good enough for what we typically want out of a formalization, but it falls short of saying that the formalization perfectly expresses the informal version of the statement.

If you want another example of an aspect of mathematical practice that cannot be quite captured by a formal system, how about inexhaustibility, in the sense of Torkel Franzen's book? To quote Goedel, "It is impossible that someone should set up a certain well-defined system of axioms and rules and consistently make the following assertion about it: All of these axioms and rules I perceive (with mathematical certitude) to be correct , and moreover I believe that they contain all of mathematics. If somebody makes such a statement he contradicts himself. For if he perceives the axioms under consideration to be correct, he also perceives (with the same certainty) that they are consistent. Hence he has a mathematical insight not derivable from his axioms."

[Timothy Chow]

Or for a different type of example, how about what Thurston asked on MathOverflow, about the distinction between how we think about mathematics and what we say out loud? If even natural language is insufficient to express everything about mathematics, then formal language is certainly going to be insufficient.

[Kevin Buzzard]

Oh I see, you're saying the formalization has more than the informal proof? Then yes I agree with you!

And I also agree with Kim -- I'm sure I've made plenty of vague but possibly helpful comments in papers which go alongside the proofs of the theorems.

[James E Hanson]

Kevin Buzzard said:

I think it certainly makes sense that mathlib should end up as a "canonical" source for every mathematical definition being used today.

This is a ridiculous idea.

[David Michael Roberts]

One might draw parallels between mathlib and Bourbaki

[Oliver Nash]

@James E Hanson Please refrain from making remarks such as the one above.

Your only contribution to this otherwise very interesting thread has been an unqualified dismissal of one person's remark in language which could reasonably be considered insulting.

We do have a code of conduct, we expect everyone to obey it, and we enact suspensions on accounts of people who do not.

[James E Hanson]

@Oliver Nash May I respectfully elaborate on why I made that comment?

[Oliver Nash]

Absolutely! I'm sure you have many great points to make and I'd love to hear them. We just want to keep things cordial and respectful!

[Kim Morrison]

(Just to clarify. Ideas can indeed be ridiculous, and it's good and fine to explain this when it happens. The problem is just that "This is a ridiculous idea", while literally being just about the idea, is easy for a reader to interpret as "The author of this idea is ridiculous", which we should go out of our way to avoid. Adding the elaboration that makes the distinction is worthwhile. I'm actually keen to argue that this idea is not ridiculous, but on the other hand I don't want to go near something that could be, or could be seen to be, involving personal animosity.)

[Oliver Nash]

This continued discussion has reminded me that I wanted to highlight to Johannes that the idea he describes here:
Johannes Schmitt said:

it might be useful that some mathematical notions do not just have one, canonical definition, but a very tightly connected cluster of definitions

is indeed something we do. Like to take a random example of something which can be defined many ways, I might take a perfect field. And you'll see that we have both docs#PerfectField and docs#PerfectRing (as well as the glue between them) etc.

[James E Hanson]

I think that it's a ridiculous idea in two ways.

The first is that I don't think there really can be a singe "canonical" source of every mathematical definition being used today. There is far, far too much mathematics being written for such a comprehensive overview. The other issue is just that, even in mathematics, definitions are fairly fluid. Concepts in math can go decades without settling into a precise form that is used uniformly throughout the literature.

The second is that the restrictions of computer formalization and the limitations of Lean mean that Mathlib often has to define things in ways that are not consistent with the way they're normally conceptualized in math. Sometimes this manifests as little edge cases in definitions, like $1/0 = 0$, but sometimes it leads to the invention of entire new concepts (like that of a 'group with zero') that have never been necessary in ordinary mathematics. And there's just generally a lot of awkward bookkeeping that really shouldn't be necessary, like maintaining a formal distinction between groups and additive groups or the inability to conveniently talk about multiple distinct topologies on the same set.

[Oliver Nash]

I don't want to nitpick because I agree with much of the sense of what you're saying (albeit I think I draw different conclusions) but I would like to supply evidence against the claim that:
James E Hanson said:

the inability to conveniently talk about multiple distinct topologies on the same set.

Here is an example of this working perfectly well in the proof that a Borel-measurable set in a Polish space is analytic: docs#MeasurableSet.analyticSet (You'll need to look at the proof here to witness this.)

[James E Hanson]

I have been told on multiple occasions that definitions involving multiple topologies that I regularly use in my field would need to be changed in order to work as smoothly as possible in Lean.

[James E Hanson]

I feel like the mere fact that Mathlib needs to maintain two different notions of 'dual Banach space' proves my point. Functional analysts do not conceptualize the dual of a Banach space as two different objects. They conceptualize it as a single object with two (or more) topologies.

[Johannes Schmitt]

Oliver Nash said:

This continued discussion has reminded me that I wanted to highlight to Johannes that the idea he describes here:
Johannes Schmitt said:

it might be useful that some mathematical notions do not just have one, canonical definition, but a very tightly connected cluster of definitions

is indeed something we do. Like to take a random example of something which can be defined many ways, I might take a perfect field. And you'll see that we have both docs#PerfectField and docs#PerfectRing (as well as the glue between them) etc.

Thanks so much for pointing this out! One thing I had in mind when I made that description: I seem to remember hearing an anecdote describing a case where for some established definition in Mathlib it became clear a posteriori that it had some quirks that made it hard to work with in practice. So the definition was changed to a more workable one, but then many things broke simultaneously and had to be manually fixed (each fix being simple, but the number non-trivial). I was just wondering why one would then not introduce the new definition as a separate entity (maybe swapping names with the old one with a pure Search-Replace on the codebase), put in the glue between them and just decide to use the new one henceforth.

I can see that this is not aesthetically pleasing, and depending on the extent of existing usage and the quality of the glue it might not save work in the end. But If that usage is very extensive, I was wondering if there is an in-principle objection to such approaches.

Also curious whether this might help with @James E Hanson 's issue: having both the math-community definition and the Lean-workable definition, and writing tight glue between them so that users can work with the math-y definition, but the glue guides Lean to the structurally more amenable one while routing its proofs.

[Sorry if I am taking in very vague terms - very interested in this topic and learning more, but still very inexperienced in the technical background and practicalities!]

[James E Hanson]

In any case, this is why I did (and still do) find Kevin's phrasing 'ridiculous'. Mathlib cannot be the canonical reference for definitions in mathematics if it already defines basic mathematical concepts in a meaningfully heterodox way for technical reasons.

[Johan Commelin]

@Johannes Schmitt What you outline is certainly also a possible approach. And possibly one that we'll have to resort to more often in the future, as the library grows further.
But in the beginning I think it has served us well to push through these refactors immediately. Because it helps keep the library coherent, instead of fracturing.

[Oliver Nash]

I bet there is even example of what Johannes how outlined in Mathlib today, though I can't immediately think of one.

I'd also add that multiple equivalent definitions scales badly. Suppose I have a lemma which takes 5 assumptions and each assumption has 2 spellings. My lemma represents just one of the 32 equivalent variants. Some downstream user might have only a 3% chance of the spelling they need existing, and it will just be a pain if every time they want to invoke a lemma they first have to invoke a handful of equivalence lemmas.

I could imagine a future in which we formalise in some higher level language which takes care of all this and we no longer care about which definition is being used, but we're not there yet.

[Johannes Schmitt]

I'd also add that multiple equivalent definitions scales badly. Suppose I have a lemma which takes 5 assumptions and each assumption has 2 spellings. My lemma represents just one of the 32 equivalent variants. Some downstream user might have only a 3% chance of the spelling they need existing, and it will just be a pain if every time they want to invoke a lemma they first have to invoke a handful of equivalence lemmas.

Thanks! So right now, there is no way that Lean can fix those adapters itself (using the "glue") I described? And that could not be put into some tactic (taking a Lemma as an argument, and saying: try to make that fit here)?

[James E Hanson]

Johannes Schmitt said:

Thanks! So right now, there is no way that Lean can fix those adapters itself (using the "glue") I described? And that could not be put into some tactic (taking a Lemma as an argument, and saying: try to make that fit here)?

It's not that it can't be done, but rather that it's not really worth the effort in the end.

[James E Hanson]

In any case I guess another reason I find Kevin's comment ridiculous is that I cannot imagine a future in which the majority of mathematicians will accept the quirks of Lean and Mathlib as the absolute canon of what words mean in mathematics. No group theory textbook is ever going to be written with the following two definitions:

A group is a set/type $G$ together with a designated element $1$, a binary operation $\cdot$, and a unary operation $x \mapsto x^{-1}$ satisfying the following:
* For all $a,b,c$ in $G$, $(a\cdot b)\cdot c = a \cdot (b \cdot c)$.
* For all $a$ in $G$, $a \cdot 1 = a$ and $1 \cdot a = a$.
* For all $a$ in $G$, $a \cdot a^{-1} = 1$ and $a^{-1} \cdot a = 1$.

An additive group is a set/type $G$ together with a designated element $0$, a binary operation $+$, and a unary operation $x \mapsto -x$ satisfying the following:
* For all $a,b,c$ in $G$, $(a+ b)+ c = a + (b + c)$.
* For all $a$ in $G$, $a + 0 = a$ and $0 + a = a$.
* For all $a$ in $G$, $a + -a = 0$ and $-a + a = 0$.

This would be patently absurd. It would literally be bad pedagogy, but it's a technical necessity in the inner workings of Mathlib.

[Johan Commelin]

Johannes Schmitt said:

Thanks! So right now, there is no way that Lean can fix those adapters itself (using the "glue") I described? And that could not be put into some tactic (taking a Lemma as an argument, and saying: try to make that fit here)?

Not in general. Although there are specific examples of this, that help generate variants of a given lemma.
For example the to_fun attribute, and the to_additive and to_dual machinery might also be seen as instances of this. In a different direction there is reassoc, which is also available as term macro, allowing it to take a lemma and "reassociate" on the fly (for a precise meaning of reassociate).

[Bryan Wang]

I personally find the comparison of mathlib to Bourbaki quite psychologically helpful. I'm sure Bourbaki has its quirks which mathematicians have learnt to live with (or without), yet it wouldn't be unjustified to call it 'a "canonical"' reference in mathematics. Bourbaki however has the unfortunate shortcoming that one cannot make a pull request to it :P

[James E Hanson]

I don't think Mathlib can even be considered a canonical reference for definitions in mathematics when it technically doesn't consider $(\mathbb{R},+)$ to be a group.

[Johannes Schmitt]

From a purely user-experience point of view, and thinking more in terms of object-oriented languages like Python/Sagemath, I guess it would be nice if there is a UniqueRepresentation object RR and it has methods RR.group() spitting out a Group and RR.additive_group() giving an AdditiveGroup. And similarly for your example of dual vector space, you would have VVdual = VV.dual() and could then obtain a TopologicalVectorSpace with VVdual.weak_star_topological_vector_space() and similar for other suitable topologies.

Of course what I write makes no sense in the existing Lean language (I presume), just wondering what types of interactions with formal languages would go easier on the brains of mathematicians.

[James E Hanson]

My understanding is that this basically does exist already.

[James E Hanson]

Like the to_additive tactic.

[James E Hanson]

Well, I guess maybe to_additive doesn't yet do all of the things one would like it to do.

[James E Hanson]

But I'm also not really saying anything about these things being a problem from an end-user perspective. I'm saying that they are examples of the distance between Mathlib and conventional mathematical thought.

[James E Hanson]

These also just the 'negative' examples, places where objects lack certain properties one would expect them to have (like $(\mathbb{R},+)$ failing to be a group). There's also plenty of junk in Mathlib if you go looking for it, as in objects having more properties than one would expect them to. 'The third coordinate of the rational number $1/2$ is a bijection' is never going to be a consequence of the canonical definition of $\mathbb{Q}$:

example : Function.Bijective (1 / 2 : ℚ).3 := by
  simp [Function.Bijective, Function.Injective, Function.Surjective]

[Johan Commelin]

@James E Hanson I feel like this is getting into territory like "Is 3 a topology on 2?". I don't think it's a fair critique of Lean/Mathlib.

[James E Hanson]

Why not? People bring this up all the time when talking about the benefits of type theory over and above set theory.

[James E Hanson]

Again, I don't think these represent real usability issues.

[James E Hanson]

Clearly one can reasonably formalize mathematics in Lean.

[James E Hanson]

What I'm objecting to is the idea that Mathlib is going to be a 'canonical source for every mathematical definition being used today'.

[James E Hanson]

If, as Kevin has said to me before, $\{\{x\}, \{x,y\}\}$ can't be considered a 'canonical' definition of ordered pairs in set theory, then I feel like this kind of objection is entirely fair.

[Johan Commelin]

I know you are objecting to that. And I think you have made good points. I just don't think that last point is a good one.

[James E Hanson]

I just think that Kevin exhibits a pretty blatant and, yes, ridiculous double standard when it comes to these kinds of things. He criticizes set theory for this kind of junk on a regular basis and insists that the definitions that are used in it are not 'canonical' but then entirely glosses over analogous shortcomings in the context of Lean and Mathlib.

[James E Hanson]

To be clear though, I'm talking about philosophical and aesthetic shortcomings, not practical ones,

[Oliver Nash]

@James E Hanson Please try harder to stick the mathematics and avoid making this a discussion about people. This is your last warning.

[James E Hanson]

I understand.

[James E Hanson]

Johan Commelin said:

James E Hanson I feel like this is getting into territory like "Is 3 a topology on 2?". I don't think it's a fair critique of Lean/Mathlib.

I guess on some level I don't actually understand why you think it's that different. Is it because this example involves digging into implementation details, whereas the previous ones really are user-facing?

[Johan Commelin]

This one is much more hypothetical. The others are about code that is in Mathlib but doesn't match the informal treatment, or vice versa.

[Martin Dvořák]

James E Hanson said:

example : Function.Bijective (1 / 2 : ℚ).3 := by
  simp [Function.Bijective, Function.Injective, Function.Surjective]

The main problem with your example, IMHO, is that you write .3 to denote .den_nz afaik. This is actually my big pet peeve. I would personally ban .1 and so on, and this problem would disappear.

I apologize for bringing a hot take into a discussion that already has enough hot takes in it.

[Aaron Hill]

James E Hanson said:

These also just the 'negative' examples, places where objects lack certain properties one would expect them to have (like $(\mathbb{R},+)$ failing to be a group). There's also plenty of junk in Mathlib if you go looking for it, as in objects having more properties than one would expect them to. 'The third coordinate of the rational number $1/2$ is a bijection' is never going to be a consequence of the canonical definition of $\mathbb{Q}$:

example : Function.Bijective (1 / 2 : ℚ).3 := by
  simp [Function.Bijective, Function.Injective, Function.Surjective]

I think there's an important difference between "every mathematical definition has a corresponding 'canonical' definition in mathlib", and "everything in mathlib corresponds to a meaninful/non-junk mathematical definition or theorem"

[Dagur Asgeirsson]

James E Hanson said:

But I'm also not really saying anything about these things being a problem from an end-user perspective. I'm saying that they are examples of the distance between Mathlib and conventional mathematical thought.

At the turn of the 20th century, there was a huge distance between conventional mathematical thought and what most mathematicians nowadays would consider as rigorous proof. Maybe something similar is happening now? There are obvious problems with the current conventional mathematical thought that mathlib can help to fix

[James E Hanson]

Dagur Asgeirsson said:

There are obvious problems with the current conventional mathematical thought that mathlib can help to fix

What problems are you referring to specifically?

[James E Hanson]

Johan Commelin said:

This one is much more hypothetical. The others are about code that is in Mathlib but doesn't match the informal treatment, or vice versa.

Why is it hypothetical? This is actual code that is Init.Data.Rat.Basic.

[James E Hanson]

Do you mean hypothetical in the sense that it only could hypothetically show up on a user-facing level, but clearly hasn't yet?

[James E Hanson]

Martin Dvořák said:

The main problem with your example, IMHO, is that you write .3 to denote .den_nz afaik. This is actually my big pet peeve. I would personally ban .1 and so on, and this problem would disappear.

I think this is a very reasonable opinion, although on some level I would still consider it to be a 'junk theorem' on an ontological level that in Lean there is an empty bijection baked into the literal structure of the object being identified with $\frac{1}{2}$.

[James E Hanson]

Aaron Hill said:

I think there's an important difference between "every mathematical definition has a corresponding 'canonical' definition in mathlib", and "everything in mathlib corresponds to a meaninful/non-junk mathematical definition or theorem"

I agree that there's a difference on some level, but I also feel like there's an important similarity. For both 'technically $(\mathbb{R},+)$ is not a group, but rather an additive group (which is a different kind of object)' and 'technically one of the fields of 1/2 : ℚ is an empty bijection', the way you deal with it is by saying something to the effect of 'oh well you're not supposed to interpret what the formal system is saying that particular way'. They both ask for a certain amount of leeway in translating the literal formal system to common mathematical conventions.

[James E Hanson]

And if I'm irascible about this particular kind of thing, it's because in my opinion a lot of rhetoric that has been employed to promote type theory in general and Lean in specific relies on giving set theoretic definitions essentially no such leeway in the translation between the literal formal system and common mathematical conventions.

[James E Hanson]

People cite statements of the form $2 \in 3$ as junk theorems all the time, but $2 \in 3$ has more mathematical content than the Mathlib facts that $(\mathbb{R},+)$ is technically not a group and 1/0 = 0.

[James E Hanson]

So, I feel like I am merely applying to Lean and Mathlib the same standard of nitpicking that has been commonly applied to set theory.

[Dagur Asgeirsson]

James E Hanson said:

Dagur Asgeirsson said:

There are obvious problems with the current conventional mathematical thought that mathlib can help to fix

What problems are you referring to specifically?

For example the abundance of "folklore results", the fact that it is acceptable to "prove" theorem X by saying "this is proved in a similar way to theorem Y", the fact that your status/fame as a mathematician influences the extent to which the community accepts your claimed proofs as correct, etc

[James E Hanson]

Dagur Asgeirsson said:

"this is proved in a similar way to theorem Y"

This is a reasonable thing to complain about but I also feel like this is a good example of how far computer formalized mathematics is from being acceptably easy to mainstream mathematicians. Sometimes it really is easy to look at a given proof and adapt it to the current context.

[Eric Vergo]

James E Hanson said:

I think that it's a ridiculous idea in two ways.

The first is that I don't think there really can be a singe "canonical" source of every mathematical definition being used today. There is far, far too much mathematics being written for such a comprehensive overview.

What percentage of all canonical definitions used today can be found on the arXiv? I bet it is up there. When comparing it to lean, the information there is sparse, poorly organized, not well vetted, etc. But it is still there. If the percentage of definitions found on the arXiv is not high enough to meet your definition of ‘every’, what about considering the internet as a whole? Is that a single source? Probably not, but powerful search tools like google certainly make it feel/act like one in practice.

[James E Hanson]

Sorry, I misread what you wrote. I don't think it's reasonable to call the internet as a whole 'a single source'.

[James E Hanson]

Especially now that Google has become meaningfully less useful as a search engine in the last 5-10 years.

[James E Hanson]

And also because one of the primary issues here is coherence. The desire is to have a single reference that defines mathematical concepts in a coherent and consistent way, and arXiv as a whole and the internet as a whole do not satisfy this.

[James E Hanson]

Mathlib does largely accomplish this to the extent that it has definitions written down, but these definitions require a meaningful amount of expertise to parse (beyond what is normally required of a mathematician in a particular field) and many of them are what I would consider to be 'bookkeeping junk'.

[Eric Vergo]

The arXiv definitely lacks coherence, and maybe I should have included it in my list of differences but the point stands. We already have massive 'living' databases of mathematics that contain large swaths of what is known and we are doing the same thing, but in lean. Yes, the barrier to entry is higher and the overhead involved in upkeep of the database is encumbering. Despite all of that, it is growing, and growing at an increasing rate.

[James E Hanson]

Eric Vergo said:

Yes, the barrier to entry is higher and the overhead involved in upkeep of the database is encumbering.

I feel like these are precisely reasons why Mathlib is not going to be a 'canonical source for every mathematical definition being used today'.

[James E Hanson]

Unless you interpret the word 'mathematical' in a very narrow sense.

[Eric Vergo]

The barrier to entry is plummeting thanks to LLMS, as evidenced by the original post in this thread. I am not going to hang my hat on these things being true moving forward.

[James E Hanson]

Well, except then you're replacing a technical barrier with a financial one. I don't have access to a high-quality LLM, so I cannot personally replicate what was described in this thread.

[James E Hanson]

Am I expected to pay $200 a month to be part of 'the future of mathematics', as Mathlib brands itself?

[Kim Morrison]

James E Hanson said:

example : Function.Bijective (1 / 2 : ℚ).3 := by
  simp [Function.Bijective, Function.Injective, Function.Surjective]

This can and should be fixed by better encapsulation. PR welcome!

[James E Hanson]

Why would I contribute free labor to undermining my own rhetorical argument?

[James E Hanson]

Besides, I don't feel like this is a legitimate issue that needs to be addressed.

[Kim Morrison]

I didn't expect you to help here, don't worry. My comment was addressed to everyone.

[James E Hanson]

Like I said, it's primarily an aesthetic and philosophical one.

[Eric Vergo]

James E Hanson said:

Am I expected to pay $200 a month to be part of 'the future of mathematics', as Mathlib brands itself?

I sincerely hope that it tops out at 200, but am quite sure that it won't. Just so we are on the same page, I think this is a disaster and would strongly prefer it not to be the case.

[James E Hanson]

I'm glad to hear it, but even aside from the direct financial aspect, I'm generally uncomfortable with the idea of big tech having such a strong role in 'the future of mathematics'.

[James E Hanson]

I don't want to install Microsoft software on my computer in order to be able to do reasonably do math, for instance.

[James E Hanson]

I know that VSCodium exists, and I currently have it installed, but I haven't tried anything involving integrating it with an LLM and in general I expect there to be an added layer of friction relative to just using VSCode. (For example, I had to manually install the Lean4 plugin.)

[James E Hanson]

I've also used the Lean4 Emacs mode, but there's obviously even more friction there (on the level of integrating it with my existing Emacs setup).

[David Michael Roberts]

It seems to me there at least three nonequivalent definitions of a proper map circulating in the literature.

[David Michael Roberts]

Cf also Bourbaki's set theory, which , well, is not standard in any sense of the word

[Timothy Chow]

Many points being raised in this discussion remind me of the QED Manifesto, which was written over thirty years ago, but which is, if anything, more relevant today than it was back when it was written. For example, the intellectual property question is raised in "Objection 2." The notion that the corpus of formalized mathematics would provide "canonical definitions" of everything is not directly addressed, but if I read between the lines, the suggestion seems to be that the system should be as flexible and adaptable as possible. That is, the ideal situation would be that you should be able to do math however you want as long as it's completely rigorous, and there should be tools to translate your work into the standard framework. (Again, that's basically what I think Conway was getting at with his "Mathematicians' Liberation Movement.")

I've cited Atiyah before in a different thread; in response to Jaffe and Quinn's expressions of concern about some areas of mathematics suffering from (for lack of a better term) insufficient rigor, Atiyah said that even though he agreed with much of the substance of what they were proposing, he rebelled against what he perceived to be an authoritarian tone. It's natural to get excited about the future of Lean and mathlib, but it's also against our own best interests to exude any odor of authoritarianism.

[Timothy Chow]

Kevin Buzzard said:

Oh I see, you're saying the formalization has more than the informal proof? Then yes I agree with you!

Yes. However, I'm also saying that the formalization does not express everything that the informal proof does (i.e., "more than the informal proof" does not, in my book, mean "everything in the informal proof plus even more").

Here's another example on top of what I've already said earlier in this thread. An informal proof may begin with a heuristic sketch of the argument that, strictly speaking, is wrong, and a fortiori cannot be formalized. The ideas in the heuristic argument may generalize to other settings in a way that the formal proof does not. Terry Tao has a nice paper, Exploring the toolkit of Jean Bourgain, whose abstract begins by quoting Gian-Carlo Rota's adage that "every mathematician only has a few tricks." Those tricks cannot always be formalized without losing something in the translation.

If what I just said still seems too vague, let's take a simple concrete example of a heuristic principle: "The prime numbers are random." Well, of course, the prime numbers aren't random. Nevertheless, the heuristic principle is extremely useful for formulating conjectures and can sometimes even be turned into a rigorous proof. I don't think that "the primes are random" can be formalized, and more importantly, I think it would probably be a mistake to try to formalize it. Any formalization would likely limit the power of the heuristic.

[James E Hanson]

The conversation in the "dreams of big projects" thread made me realize that there's another reason why Mathlib simply cannot be a canonical source for every mathematical definition being used today: Mathlib cannot easily handle things like choiceless classical mathematics, weaker-than-ZF classical mathematics, or constructive mathematics (which all often involve specialized definitions). There's never going to be a structure in Mathlib for apartness relations, for instance.

Now, I'm not saying that this is something Mathlib really needs to address, per se, but I do think it makes it pretty clear that one cannot claim that every mathematical definition being used today is going to eventually make its way into Mathlib. Unless, of course, one would be willing to assert that the above things are 'not mathematics', but that's a different conversation.

[Martin Dvořák]

James E Hanson said:

I think this is a very reasonable opinion, although on some level I would still consider it to be a 'junk theorem' on an ontological level that in Lean there is an empty bijection baked into the literal structure of the object being identified with $\frac{1}{2}$.

Yes, it would still be a junk theorem. Totally junk! However, once I clearly see that it talks about some bijection between proofs, I will immediately conclude "yeah, a typical foundational quirk" and go on.

Confusion stems from not knowing what something means. And, in almost every situation, I have no idea what .3 means. This time, I knew only because I had been writing a thesis section about Rat recently.

[Simon Sorg]

This thread has gone a long way from it's initial starting point, moving far beyond feedback on the formalization that was initially requested. It might be worth to move parts of this into its own thread, and potentially into general as this is barely touching Machine Learning anymore.

[Notification Bot]

95 messages were moved here from #Machine Learning for Theorem Proving > AI-discovered proof on psi-integrals (with Lean formalizat.) by Oliver Nash.

[Edward van de Meent]

Kim Morrison said:

James E Hanson said:

example : Function.Bijective (1 / 2 : ℚ).3 := by
  simp [Function.Bijective, Function.Injective, Function.Surjective]

This can and should be fixed by better encapsulation. PR welcome!

i'm not sure this gets better by encapsulating? the third field of Rat says the denominator is not 0, an inequality is the negation of an equality, and proofs of negations are functions. All of these parts are reasonable definitions, and even if we were to encapsulate these with structures, you still will get the same kind of 'nonsense result' by inserting more projections, like Function.Bijective (1 / 2 : ℚ).3.1.1. Making these definitions opaque is definitely possible (provided we create API for casting back and forth) but that will make for absolutely horrible ergonomics

[Edward van de Meent]

can you maybe explain the fix you had in mind?

[Oliver Nash]

I suggest we try to keep this thread a bit more on topic.

IMHO there is a potentially useful conversation to be had about the pros and cons of Mathlib as a source of definitions and it will never happen if we allow ourselves to be distracted with these sorts of tangents.

[Timothy Chow]

Is it a tangent? The topic, now that it has been moved into its own thread, is the relationship between formal definitions (in a corpus that we envisage becoming "standard") and definitions used in mathematical practice. One of the main concerns that has been raised is that formal definitions are always going to be plagued to some extent by technical irrelevancies. Detailed consideration of specific examples can help illuminate this concern.

Iny any case, I suggest that we re-frame the discussion a bit. Instead of speculating about some hypothetical future world in which mathlib lays down the law for every definition, maybe we can discuss whether mathlib can be made more flexible, to reflect the flexibility of actual mathematical practice. In another discussion, I pointed out that in ZF, there are different ways to formulate the continuum hypothesis that are equivalent in ZFC but inequivalent in ZF. Aaron Liu's response was, "Well, we have choice, so." That's a reasonable perspective to take, but it potentially goes against the idea of mathlib being a universal umbrella for all of mathematics.

My impression is that the dominant philosophy so far has been that the priority has been to get as much mathematics into mathlib as quickly as possible (without of course sacrificing correctness). If that means sacrificing intuitionistic logic or choiceless math or some other area of math that is perceived to be "niche," well, that's a sacrifice we can live with (at least for the time being) because we have bigger fish to fry. Again, I'm not saying this is a bad idea, but we should be aware that we can't always eat our cake and have it, too.