Platonism in Lean?

Stream: new members

[Mr Proof]

From using Lean for the last few days, I have been struck by a bit of a philosophical problem. :thought:

This is what do we actually mean by a mathematical object?

For example consider the Octonions. There are 3 or 4 different ways to construct these. (e.g. from quaternions, complex numbers or real number parts). Thus in fact we have 4 mathematical objects:
OctonionsConstrucutedByMethodA
OctonionsConstrucutedByMethodB
OctonionsConstrucutedByMethodC
OctonionsConstrucutedByMethodD
Since we have constructed them in 4 different ways how do we know they are the same? We must construct proofs to show this. Why then should we label one of these as the "correct" definition of the Octonions? But we are forced to make that choice.
But we cannot simply ignore the other ways of constructing them since when a mathematician talks about "the Octonions" we don't necessarily know which construction they have in mind.

This is not too bad for a simple thing like the octonions but it would become more important for more abstract concepts. Take the example of Calabi-Yau manifolds. There are 6 -8 definitions. Thus what is the definition that should be formalised? Well they should all be formalised and proved to be equivalent (if indeed they are), but still we are forced to label one construction as "the" definition. The alternative would be to give all definitions their full title. e.g. CalabiYauManifoldAsDefinedByVanishingChernClass. Although that would be cumbersome.

I suppose the danger is by choosing one construction over another it may turn out that the two constructions aren't equivalent after all. The classic example being when it was found out that manifolds being homeomorphic was not equivalent to them being diffeomorphic. Two things that were thought to be equivalent but turned out not to be.

So my own view that I've come to is that mathematical objects don't exist at all. :open_mouth: Only constructions "exist".

Thanks for listening to my ramblings. :grinning:Any thoughts on this?

[Damiano Testa]

I personally take a different view: mathematical objects do exist. To talk about them, it is convenient to express them in some way and that is an implementation detail. You make sure that you have implemented the correct representation of you ideal object, by proving properties of that definition.

[Kevin Buzzard]

The different methods give you objects which are "the same" in the sense that they are isomorphic. Mathematicians don't usually distinguish between isomorphic objects (they don't care at all whether their real numbers are Cauchy or Dedekind). Yes there will be one "definition" of a thing (for example mathlib's definition of "compact" is "every Cauchy filter converges") but if you want to use a different definition (eg every open cover has a finite subcover) then this is a theorem in the library which you just apply and you don't care if the proof is rfl or not because that's an implementation detail. A calabi yau over a field is a morphism of schemes which satisfies one of 6 mathematically equivalent predicates and yes you just prove they're all equivalent and then move on.

[Jason Rute]

First, I don’t think #lean4 is the right place for this topic. (Maybe #new members. A moderator could move it.). Second a good book on this topic is _Thinking about mathematics_ by Steward Shapiro. To Kevin’s point, I like the position of Structuralism, which sort of says the definition and existence of a mathematical object is inextricably tied to the structure it is part of, and that to whatever sense mathematical objects “exist” it is only up to isomorphism.

[Jason Rute]

My advisor Jeremy Avigad is a philosopher of math (among many other things), and has been a huge proponent of making philosophy of math into a practical subject.

[Jason Rute]

For example, while I think discussing platonism in mathematics can only go so far, there are a lot of important practical questions about definitions in mathematics, especially in a formal mathematics:

• For every object is there a right definition we should be converging to? (I’ve heard some in this community expose this point of view.)
• When we define an object, should we only define it up to isomorphism? For example, we could construct the reals as a specific quotient of another type, or we could take a more axiomatic point of view defining the reals as a complete ordered field (of which there is only one up to isomorphism).
• In homotopy type theory with Univalence (or with cubical type theory), any pair of isomorphic objects are equal, so this means in some sense it doesn’t matter what our original definition was, since we can replace it with an isomorphic one. But others have expressed that working with univalence isn’t really practical.)
• In intentional dependent type theory (on which Lean is based) we put a lot of emphasis on the original definition since it is important for definitional equality, but that is also weird given the above. In Metamath, HOL, and extensional dependent type theory, they don’t have as strong of a problem here, since a definition is basically just a theorem. So it doesn’t matter which definition of the prime numbers is the original definition in the library. (However, one reason we also like definitional equality is because it naturally leads to computation.)
• Many definitions in proof assistants are ugly for practical reasons. For example, Lean defines 0/0=0. Are there practical and beautiful alternatives (maybe in a new formal system)?
• Should we try to define a mathematical definition in the most generality?
• How do we practically translate (or interface) mathematical libraries which have different definitions of the same mathematical objects (sometimes where the definitions of the same object have different levels of generality or are not even isomorphic).
• How do we leverage AI to translate informal math into formal math, especially if it has to formalize new definitions? How can we be sure the definition isn’t translated vacuously? Is it more important that the definition is translated faithfully to the original or translated into the most beautiful, general form given the above concerns?
• How do we represent mathematical definitions in AI? What can AI’s “understanding” of mathematics, including definitions and proofs, tell us about our own?
• Should definitions in formal libraries be static things which remain fixed (for practical concerns like referencibility) or should they be organic and changing just like in real mathematics where we are constantly iterating on definitions to make them better? (Actually real mathematics has both. Every paper has whatever definition it uses, fixed to an article with a citation, but the definition itself is constantly evolving across papers.)

[Mr Proof]

Interesting... :thinking:
I do think it's actually quite an import practical problem that goes to the heart of proof assistants. Because the very purpose of proof assistants is that they can be trusted. And we can 100% trust that given a statement in Lean if we can provide a certificate then the statement is proved. My worry is, that although the statement is proved, without knowing the definition of every word in the statement we might not be actually proving what we thought we were proving!
When the statement itself is trivial (e.g. FLT) the definitions of things in the proof steps don't really matter. I can trust that the statement of FLT is what it says it is because I can understand the definitions of every word in the statement.

The thing I worry about is when the proposition itself uses definitions that rely on a whole tower of choices of definitions. Then it becomes less clear if the proof would still be valid if a different set of choices had been made.

In practical terms, I think proof assistants work best when the statement you are trying to prove can be stated trivially (like FLT :+1:), but that all other statements should be classed as "useful" in that they can be used for lean proofs for human consumption but viewed with a bit of scepticism when used in the statement you are trying to prove . I recall a real world example where two papers had proved the exact opposite of each other due to one particular choice of definition which was slightly more general the other. So in fact they were both right, it's just that they had proved different things!

[Jason Rute]

This question of whether one has the right definition was a big concern in the LTE (cc @Johan Commelin and @Adam Topaz ) and they put a lot of work into showing that the definitions behaved as expected).

[Kevin Buzzard]

https://leanprover-community.github.io/blog/posts/lte-examples/ was the blog post.

[Martin Dvořák]

I am a formalist and I always care about the definition. Let's say there are two equivalent definitions defA and defB and, to make things simpler, they are both of the type ℚ → Prop. Even tho we have proved that defA and defB are equivalent, I still care about which is the definition of the object I work with. Let's say there is a bigger structure with a field whose type is either defA or defB. My belief is that, if I work in terms of defB whereäs the definition is in terms of defA, I must call the lemma that translated between them; if I don't refer to the conversion lemma, my proof is incorrect. And yes, my point if view had been this rigid even before I found Lean.

[Philippe Duchon]

I would be of the opposite conviction - it is not important to know what a X is, only "how it works". If I know that two different definitions of an X are in fact equivalent, then I don't really care which is the definition and which is the theorem. Occasionally, I will be happy to work with both definitions - after all, they are equivalent.

Then when it comes to writing a formalization, I would expect the people to pick the definition that best integrates into the existing hierarchy, and also provide the other as an equivalence theorem. I don't have the level of familiarity with the library and its mechanisms to decide which is best, so for the moment I'm happy to leave this kind of decisions to those who know (or who are confident enough to say they know).