Univalence

Stream: maths

[Bas Spitters]

I believe univalence can consistently be added to lean, since classical logic is valid in the simplicial set model
(https://www.math.uwo.ca/faculty/kapulkin/notes/LEM_in_sSet.pdf).
Moreover, that model also interprets strict propositions.
One would of course need to disable UIP for universes. Would that be possible?

[Chris Hughes]

Have you seen https://github.com/gebner/hott3 ?

[Kevin Buzzard]

I thought that the issue was that bool = bool was a singleton in Lean but bool \equiv bool was not.

[Chris Hughes]

That's why you have to disable Prop, or at least large elimination from Props

[Chris Hughes]

And redefine equality to be a Type

[Kevin Buzzard]

and this breaks all of mathlib immediately, right?

[Chris Hughes]

Yes

[Kevin Buzzard]

and also it means that it would be much harder to make it all again, because the cool tricks we can get away with because any two terms of type P : Prop are equal won't work any more, so it might not even be possible to make parts of mathlib again if we have univalence.

[Reid Barton]

I understand why equality can't be a Prop but once that is changed I don't understand why Prop itself causes any problems.

[Mario Carneiro]

If eq : A -> A -> Prop exists then you can prove that eq' : A -> A -> Type is equivalent to it and hence also satisfies UIP

[Chris Hughes]

Because this is inconsistent right?

inductive eq2 {α : Type} (a : α) : α → Type
| refl : eq2 a

example {α : Type} (a b : α) (h₁ h₂ : eq2 a b) : eq2 h₁ h₂ :=
by cases h₁; cases h₂; exact eq2.refl  _

[Mario Carneiro]

which is basically what Chris's proof does, because cases is implicitly using eq

[Reid Barton]

I was going to say maybe this just means you need to adjust the rules for large elimination of Props to not allow smuggling in eq, but possibly that eliminates all interesting uses?

[Mario Carneiro]

If prop looked like type there wouldn't be any issues

[Reid Barton]

Well then it might as well not exist, right?

[Mario Carneiro]

I am not sure if the impredicativity is also bad but if you don't have UIP in prop then I think it would be bad

[Reid Barton]

I guess the question is how much stuff can you put into a definitionally proof-irrelevant Prop while remaining consistent with univalence, and is that amount enough to be useful

[Mario Carneiro]

You could remove all large elimination. just have all inductive types act like exists

[Mario Carneiro]

then Prop becomes a one-way path so it can't cause problems... I hope

[Reid Barton]

Right, I should go back to: how permissive can the large elimination rules be

[Reid Barton]

E.g. I imagine that large elimination for true is ok

[Reid Barton]

But it's also not that exciting

[Mario Carneiro]

Some large elimination principles are provable without assuming them, like and

[Reid Barton]

There's surely going to be issues with propext next, I guess

[Mario Carneiro]

but those are basically the only okay ones

[Reid Barton]

Oh maybe there is no issue with propext as long as its type itself doesn't have large elimination

[Mario Carneiro]

propext is actually univalence for propositions

[Reid Barton]

Ok, I think what I was imagining is not a real issue

[Reid Barton]

I guess if you can track the h-levels of types syntactically then you can also allow large elimination when appropriate. Is this what Arend does?

[Reid Barton]

Hmm this isn't very obvious actually

[Kevin Buzzard]

This theorising is all well and good but you seem to be saying "if lean's core logic is changed a bit then it would be interesting to see what still works" and I'm merely pointing out that it might be much much harder to develop a proper maths library, which is my impression of what happens the moment you go univalent: you can compute homotopy types of synthetic spheres and then the only thing you can do is higher topos theory

[Kevin Buzzard]

Because you can't use cases any more

[Mario Carneiro]

in principle, lean tactics could be modified to be less HoTT-unfriendly. In practice, the people who are capable of doing a good job of it are not interested

[Bas Spitters]

@Chris Hughes Thanks. Does one still have classical logic?
Instead of singleton elimination, I guess one wants this: @Gaëtan Gilbert is also involved in that.
https://jesper.sikanda.be/files/definitional-proof-irrelevance-without-K.pdf

[Bas Spitters]

@Kevin Buzzard Most of basic maths happens at the lowest type level, so things wouldn't change much. Only the first universe becomes a groupoid, the second a 2-groupoid, etc.
One would notice it when formalizing presheaves, and there I would expect it to be the more natural thing to do. Unless one is "evil":
https://ncatlab.org/nlab/show/principle+of+equivalence

[Kevin Buzzard]

Presheaves are just a fancy word for functors and I'm sure there will be no problems with functors in a HoTT theory. I want to go much further than this. I want to see the proof that the presheaf of rings on an affine scheme is a sheaf, ie not just a definition of presheaves but a proof that they can be used. This took a team of complete amateurs a few months in Lean -- we were all mathematicians who knew nothing about computer proof systems or type theory one year earlier. I genuinely don't know whether the reason this isn't done in any computer HoTT system is because the systems aren't capable or because there just isn't anyone interested in doing it. I believe that there are classical hypotheses everywhere in the argument.

[Kevin Buzzard]

The reason I am banging on about this is that if your original assertion is supposed to imply that adding univalence does not in theory break anything, then I am pointing at an explicit piece of MSc level mathematics whose proof will be completely broken by it and am trying to ask the question "is there any evidence that it can actually be fixed in practice?". I am arguing that it took a team of amateurs a few months to make this proof in Lean in their spare time, so it does not seem like an unreasonable practical challenge. In my mind, one of the main things lean has going for it is a whole bunch of examples of mathematics at MSc level and above being done with relative ease by the community -- a proof that the proof assistant is usable in practice to do "fashionable mathematics".

However this might well be a long way from the point you were trying to make originally and so I'll now stop banging on about this on this thread. Sorry to derail.

I think Chris' original comment on Gabriel's work on HoTT in Lean 3 is the place to start. Both he and Floris van Doorn are experts in doing HoTT in Lean, but currently I don't think either of them are doing any, and perhaps this is only because the community is not there yet.

[Kevin Buzzard]

I could envisage someone setting an undergraduate project on doing some HoTT formalisation in Lean using Gabriel's library and then a stream being set up here for HoTT In Lean and one could just see how easy it is to do mathematics in practice in this mode. It would definitely be an interesting and worthwhile project. One could imagine the UniMath library and the HoTT book as being useful resources and one could ask whether this Lean framework is easier to use than the corresponding Coq framework

[Bas Spitters]

Of course, I would start from the HoTT library, not UniMath. It is better engineered and doesn't have the imho arbitrary restriction on the use of e.g. record types.
https://github.com/HoTT/HoTT

[Kevin Buzzard]

Thanks for reminding me of this library! I see that it is actively growing too :D People are currently thinking about groups, judging by recent commits. Can you state Sylow's theorems? Can you prove them?

To give you some sort of data point for comparison, when I arrived at Lean they had in their maths library a theory of groups, rings and topological spaces, and a good theory of finite sets. They had the naturals, integers, rationals and reals, and perhaps not too much more of interest to a "working mathematician" (although my memory might be inaccurate). This was definitely enough to get me interested though. Within a year Chris Hughes had proved Sylow's theorems, and he was a 1st year undergraduate mathematician with training in computer proof systems; Kenny Lau had set up a theory of localisation of rings, and he was also a 1st year undergraduate mathematician with no prior training in computer proof systems, and the three of us had proved this result about schemes. The reason I'm mentioning it is that one could ask what the "bare minimum"is that one needs to get mathematicians involved. And in my experience it's undergraduate mathematicians you can start with, especially when you say to them "hey there's this cool system and there's a whole bunch of undergraduate level maths in it which you can do and which we need".

Are you considering the possibility of porting this library to Lean? Is that the question you're really asking -- whether the logics of the systems are sufficiently compatible?

[Chris Hughes]

Impredicativity isn't compatible with HoTT right? This is something that seems quite important to do normal maths.

[Mario Carneiro]

Actually, impredicativity can be done in HoTT but it doesn't look the same. There is a well known result that says that two impredicative universes is inconsistent, and one impredicative universe is System F which does not have the "standard semantics" we like to have for function types and such. In the standard HoTT foundations you can define what it means for a type to be a proposition, but you end up with a subset of the universe at each level that are propositions, and there may be "more propositions" at the higher levels; this is what we mean by predicativity.

In order to reflect these propositions down to the lowest level to get something more impredicative, there is Voevodsky's "universe resizing" rule. IIRC it says that if A : Type u and is_prop A (which we would render as subsingleton A), then there exists A' : Type 0 such that equiv A A' (and a forteriori is_prop A' as well).

[Mario Carneiro]

In classical logic, this is trivial, because every proposition is either true or false and both true and false can be found in the lowest universe.

[Bas Spitters]

@Chris Hughes
Impredicativity is called the resizing axiom in the HoTT book. It holds in most (classical) models of HoTT, e.g. simplicial sets.

[Mario Carneiro]

But it is an axiom, yes? This by contrast to the way lean's impredicativity works, by a different typing rule for the Pi

[Bas Spitters]

@Mario Carneiro In the simplicial set model, the hProps are not the booleans, so the issue is somewhat more subtle:
Any contractible type is equivalent to a point (e.g. the unit type in the lowest universe)

[Mario Carneiro]

I suspect that Kevin et al really want the hProps to be equivalent to bool

[Bas Spitters]

One could use strict propositions for that, as developed by @Gaëtan Gilbert in Coq

[Mario Carneiro]

is there a motivating example for why hProp can't be bool, in a classical HoTT model?

[Mario Carneiro]

I would have thought equality would be an example but it's not even an hProp unless the type is a hSet

[Mario Carneiro]

I'm not really sure how strict propositions (by which I assume you mean Coq's SProp) differs from lean's Prop, and in particular what they do to avoid the exact same constructions shown by Chris above that trivialize the equality relation

[Bas Spitters]

@Mario Carneiro @Chris Hughes Indeed, with classical logic, hProp ~ bool. Cor 4 of:
https://www.math.uwo.ca/faculty/kapulkin/notes/LEM_in_sSet.pdf

[Johan Commelin]

@Bas Spitters Does this mean that we can assume all types (or at least all types X with is_Set X) are either empty or have a term?

[Bas Spitters]

@Johan Commelin Yes, that should be provable. Assuming classical logic and choice, hSets form a model of Lawvere's structural set theory.

[Johan Commelin]

Maybe with the new tooling it becomes easier to switch back and forth between mathlib and the hott3 project...

[Johan Commelin]

I wouldn't mind playing with it.

[Bas Spitters]

@Mario Carneiro Consider a huge type what paths between all terms. This is contractible, so an hprop, but this is obviously not a boolean.

[Mario Carneiro]

isn't it equivalent to true?

[Mario Carneiro]

what makes it "huge"?

[Mario Carneiro]

or are you saying it has higher structure like loops or something

[Bas Spitters]

@Johan Commelin We can also consider the universe of strict sets. Here is a constructive development, which will not be easy to read, but may give an idea of the type theory.
http://www.cse.chalmers.se/~coquand/bishop.pdf

[Johan Commelin]

What is the difference between an hSet and a strict set?

[Mario Carneiro]

two equalities of fixed values in a strict set are defeq

[Mario Carneiro]

in other words, lean types

[Johan Commelin]

Aha... but can you have those in a HoTT system?

[Mario Carneiro]

that is based on skimming Bas's link

[Mario Carneiro]

I don't think that type theory is classical, although probably you can just throw that in

[Mario Carneiro]

but the upshot of all this is still not clear to me. It sounds like you are offering most of the features lean has already. What are we giving up? Clearly something has to give since univalence in lean is disprovable

[Mario Carneiro]

the stuff about simplicial sets or cubical set models is not relevant for the lean user, since we are working in the theory not on the theory. (Formalizing type theories would be a worthy project but quite independent of tweaks to lean foundations.)

[Bas Spitters]

One would have a type theory with two kinds of propositions, strict ones and hProps.
set level mathematics should go through at the bottom universe, but the other universes can be univalent.
So one would need to give up UIP for the higher universes.

[Mario Carneiro]

Wait, so the lowest universe is not univalent in this scheme? Isn't that where all the interesting maths would go? For example, I guess one desideratum would be to have real = real x {0} be provable, as well as similar statements for the corresponding elements of a fully bundled type Ring := Sigma (A : Type 0) (mul : A -> A -> A), .... As I understand it this is the main selling point of having univalence around, but these objects are h-sets, possibly strict sets if you prefer, and live in the bottom universe. (Ring lives in the next universe but equality of rings, which should mean ring isomorphism, depends on equality in Type 0, and so needs the bottom universe to be univalent.)

[Mario Carneiro]

While UIP is tremendously convenient, it doesn't actually enable any particular kind of maths, as long as you can obtain the (non-judgmental) equality by other means. It would still require a lot of engineering effort to recover the same level of ease of use that you get with UIP, but at least in principle I can see giving it up provided that things like the resizing axiom are around to allow us to do long well founded recursions and such.

[Reid Barton]

I think @eq A a b is a Prop if A : Type 0. That doesn't prevent Type itself from satisfying univalence

[Bas Spitters]

We could have a universe of strict sets, and a universe of hSets living side by side.
@Gaëtan Gilbert has been working on the type theory for this. Some things will simplify in the classical model of simplicial sets, but I'm not sure anyone has gone through the details. It will be a simplification of Thierry's note.

[Johan Commelin]

What would "living side by side" mean in practice? Would it be easy to transport data and properties from one side to the other? Or would the gap be about as big as the gap between two different libraries right now (e.g., mathcomp and mathlib)?

[Bas Spitters]

This paper discusses a decade long research program on implementing transfer in proof assistants (Coq, Isabelle,...)
The Marriage of Univalence and Parametricity
https://arxiv.org/abs/1909.05027
and claims that the approach using HoTT is most convenient. It would be interesting to know whether there are any initiatives to implement transfer in lean.

[Johan Commelin]

@Cyril Cohen has been working on this about a year ago.

[Bas Spitters]

Reference?

[Johan Commelin]

But so far we don't have any usable tools.

[Johan Commelin]

https://github.com/CohenCyril/mathlib/commits/param

[Bas Spitters]

I guess that is the CoqEAL approach? Has it been proved to work with classical logic? I don't recall seeing that result explicitly.

[Johan Commelin]

I really don't know.

[Johan Commelin]

This is stuff that I never thought about as a mathematician

[Johan Commelin]

It's just an extremely annoying problem that you discover once you start using ITP's

[Bas Spitters]

@Johan Commelin I don't think the type theory has been worked out. It would be somewhat like the interaction of sProp and Prop in Coq and agda.
Semantically, we can check what is going on by looking at the classical groupoid model.

[Bas Spitters]

Strange, I would imagine you would know about Artin gluing
https://drops.dagstuhl.de/opus/volltexte/2019/10532/pdf/LIPIcs-FSCD-2019-25.pdf

[Johan Commelin]

I think it would be very helpful if some HoTT library would demonstrate that it's useful for maths that doesn't look like homotopy theory. It doesn't have to be perfectoid spaces. But something like the Hilbert basis theorem, or even better fundamental theorem of calculus. Those are low-level from a maths point of view, but my impression is that they are currently challenging for HoTT libs.

[Johan Commelin]

Hmmm... let me check that link

[Bas Spitters]

Unary, binary and machine integers low level enough for you :-)
That's the examples they look at in the univalent parametricity paper.

[Johan Commelin]

@Bas Spitters Ok, I've heard of things like gluing sheaves or topoi, or what not. But (for a simple mathematician) it's not clear how that helps us with $A$ and $B$ are isomorphic semirings, $B$ is a noetherian integral domain, hence $A$ is as well.

[Johan Commelin]

And mathematicians completely don't know what you need to do to prove such a statement. They only know a 1-word proof: "Obvious".

[Johan Commelin]

Bas Spitters said:

Unary, binary and machine integers low level enough for you :-)
That's the examples they look at in the univalent parametricity paper.

No, that won't do. We need to know that the maths that appears in bachelor courses is at least as easy in HoTT as it is in DTT like Lean.

[Bas Spitters]

@Johan Commelin There was a smiley missing in my last comment. I just wanted to point out that the "annoying problem" actually hides beautiful maths that you know well.

[Johan Commelin]

So it has to be some calculus or commutative algebra or something. Binary integers are too low level.

[Johan Commelin]

Sure... but I'm talking about the public relations / advertisement side of things. To get things rolling you need an eye-catching result.

[Bas Spitters]

Here are some examples from algebra:
http://www.cse.chalmers.se/~nad/publications/coquand-danielsson-isomorphism-is-equality.pdf
We are currently working on a formalization of universal algebra in HoTT. The isomorphism theorems become "identification theorems".

[Kevin Buzzard]

This is not what is taught in 1st year undergraduate classes. What Johan and I are trying to say is this: if HoTT is supposed to be able to do mathematics, let's see some mathematics which are taught in standard undergraduate mathematics classes. Where is quadratic reciprocity in any HoTT theory? The proof of this is not straightforward. You need a robust theory of finite sets. You need to be able to count. Where is the proof of Lagrange's theorem? Where is "normal mathematics"? machine integers and universal algebra etc are exactly what we are not talking about.

[Kevin Buzzard]

Navel-gazing about equality is something else which is not done at all in a mathematics department, away from esoteric coursees.

[Bas Spitters]

We may be talking past eachother, but I am saying that in HoTT we can prove @Johan Commelin s statement about integral domains by univalent transfer. Since, A and B are ismorphic algebraic structures, the record types are equal, and hence we can transport the property of being a noetherian integral domain.

[Johan Commelin]

Exactly! And that is why HoTT is so enticing!

[Johan Commelin]

But if that is the "only" thing it can do... it's no good (of course I'm exagerating with "only").

[Johan Commelin]

We need a system that gives us a powerful transfer. But we also need a system that gives us quadratic reciprocity, fund.thm.calc., lagrange, hilbert basis, and all the rest.

[Johan Commelin]

So far we have all the classical (not in the logic sense, but in temporal sense) systems that struggle with transfer, and we have HoTT which doesn't.
But HoTT isn't proving that you can do the "classical" theorems of mathematics in it.

[Johan Commelin]

Universal algebra is nice. But can it be applied?

[Johan Commelin]

If you can give me a formalisation of quadratic reciprocity as a 10 line consequence of universal algebra. Sure, then I will be very excited about the universal algebra library.

[Johan Commelin]

Especially if the fundamental theorem of calculus is another 30-line consequence

[Johan Commelin]

But I doubt that that is true.

[Johan Commelin]

To use some categorical language: we want the pushout of HoTT and mathlib.

[Johan Commelin]

We need another paper "The marriage of univalence and material set theory".

[Bas Spitters]

I am aware universal algebra is close to logic/CS. I.e. it's use in effectful computation.
My PhD-student Andreas has been working on integrating math-comp and HoTT.
This is currently stuck on universe polymorphism:
https://github.com/coq/coq/issues/10513
Perhaps Coq is trying to be too clever, and the more conservative approach of lean would work better. Also, there is less legacy code in lean.

[Bas Spitters]

Theorem 10.1.15 of the HoTT book:
If the axiom of choice holds then the category Set is a well-pointed boolean elementary topos with choice.

This is called Lawver set theory. What else do you want from set theory?

[Johan Commelin]

I think that's good. That's good enough for the theoretical foundations. What we need to see is that it's usable in practice.

[Johan Commelin]

How many lines of code does mathlib use to prove quadratic reciprocity? (I dunno, but we can find out.)
Can we do a 1-1 translation to HoTT?

[Johan Commelin]

If not 1-to-1, what is the factor that proofs scale by? Should we expect less lines of code, or more?

[Johan Commelin]

That's the kind of question that Kevin and I are interested in.

[Johan Commelin]

Of course we could try to figure this out ourselves. But we are also wondering why HoTT experts are not figuring this out.

[Johan Commelin]

(Also, unfortunately I need to spend lots of time on paper maths projects, and diving into developing a theory of finite sets in HoTT would not make my boss happy.)

[Sebastien Gouezel]

I have the following analogy. It is consistent with ZF to assume that every set of the real line is measurable. Then, one can add this axiom, and do all measure theory in an extremely nice way (much nicer than what is usually done because you won't need to check measurability any time). Except that then you can not integrate this measure theory library with other traditional parts of maths that require choice (for instance the existence of the algebraic closure), as assuming measurability of everything is contradictory with choice. In this situation, it seems to me that doing measure theory in this way would be cheating, and mostly useless to build a whole library of mathematics.

As to whether this is a good analogy with HOTT, I won't say anything, because I don't understand anything to HOTT.

[Bas Spitters]

Unless, I am overlooking something, lean is already consistent with HoTT under this translation (which uses --indices-matter)( @Gaëtan Gilbert ?)
https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581
Of course, that does not directly give univalence, but it embeds lean in the strict propositions that we discussed before.

[Mario Carneiro]

Yes but Coq isn't HoTT, it's some poorly defined union of a bunch of type theory extensions

[Bas Spitters]

@Mario Carneiro Coq implements pcuic. What do you mean?

[Mario Carneiro]

Coq doesn't "just" implement pcuic, it has extra stuff

[Mario Carneiro]

I have literally never seen a definition of Coq that didn't finish "oh and there's also some other stuff we won't go into here"

[Mario Carneiro]

I'm not 100% positive I know what the exact theory you are calling PCUIC is (usually people call "that thing Coq implements" CIC instead) but I think that SProp is not mentioned in it

[Gaëtan Gilbert]

Unless, I am overlooking something, lean is already consistent with HoTT under this translation (which uses --indices-matter)( @Gaëtan Gilbert ?)

I'm pretty sure the translation breaks when using -indices-matter
Lean can't be consistent with HoTT since Lean has UIP

[Bas Spitters]

@Gaëtan Gilbert What is the status of strict sets?

[Bas Spitters]

Pcuic:
https://hal.inria.fr/hal-01615123v2/document
SProp is a recent addition described in Gaetan's thesis.

[Mario Carneiro]

I know

[Mario Carneiro]

hence my claim that it's the union of a bunch of type theory extensions that have not all been examined as a whole

[Mario Carneiro]

I really sincerely don't understand why there isn't some reference linked from the coq manual or something that defines the whole axiomatic system and stays up to date with new versions

[Bas Spitters]

@Sebastien Gouezel First, besides your point, measure theory should be developed algebraically/categorically e.g. in line with the theory of von Neumann algebras. See the remarks by people like Rota and Tao.
But to address your point, which axiom would you like to add that is inconsistent with lawvere set theory ?

[Johan Commelin]

All this talk about foundations is nice and well. My question remains: suppose that all of mathlib were translated by magic to HoTT. Would it be longer or shorter?

[Bas Spitters]

It should be shorter, as we have more axioms (UA) at our disposal. However, I cannot completely gauge the influence of strict equality at the moment.

[Johan Commelin]

The number of axioms is not the only factor. We lose definitional proof irrelevance. Will automation apply it for us instead? How often will I need to prove that my type is an hSet? Or is that automated? Is there type class inference? Is there a simplifier? Do they work?

[Mario Carneiro]

for that argument to work, you have to be able to mimic/model/implement every single one of lean's axioms and defeqs. The "coq is a lean typechecker" suggests that this is very nearly possible, but it seems like you still have to give up some things, like lean's strong form of the axiom of choice

[Johan Commelin]

But "coq is a lean typechecker" was not a univalent coq, was it?

[Mario Carneiro]

no

[Mario Carneiro]

I think Bas is claiming that there is a way to have both strict sets and univalence in the same system

[Mario Carneiro]

but I'm pretty sure that nonempty A -> A breaks everything

[Mario Carneiro]

the hott version of the axiom of choice is much more guarded, something like (Pi x, nonempty (A x)) -> nonempty (Pi x, A x)

[Sebastien Gouezel]

Bas Spitters said:

Sebastien Gouezel First, besides your point, measure theory should be developed algebraically/categorically e.g. in line with the theory of von Neumann algebras. See the remarks by people like Rota and Tao.

It definitely shouldn't. The von Neumann algebra point of view is interesting, but there are many statements of down to earth measure theory that are just not true in this generality.

[Sebastien Gouezel]

Bas Spitters said:

But to address your point, which axiom would you like to add that is inconsistent with lawvere set theory ?

As I was saying, I don't know anything about HOTT. But my impression as an outsider is that you have to sacrifice some versions of choice, which is not an option for me. I would be happy to be proven wrong!

[Mario Carneiro]

By the way, lean's version of the axiom of choice isn't even ok in ZFC. It's known as "global choice", positing the existence of a proper class function that is a choice function on every set

[Mario Carneiro]

The actual axiom of choice only allows you to choose from set-many nonempty sets at once

[Mario Carneiro]

However, in set theory you do have definable definite description, so unlike lean you don't have to use choice to define things like lim when the limit is unique

[Gabriel Ebner]

I'm not sure this is true though since a Lean term can only talk about finitely many choice constants. Lean has a choice.{u} constant for every universe u. There is no relation between choice.{u} and choice.{u+1} (except for what you get out of the type). And each choice.{u} is definable in ZFC + enough inaccessibles.

[Mario Carneiro]

Oh, that's an interesting point

[Mario Carneiro]

Still, choice.{-} has a bit of a peculiar status as a family then, since it will not be uniformly definable

[Gabriel Ebner]

Is Type.{-} uniformly definable?

[Mario Carneiro]

In all the models that I've considered for lean in set theory, yes. It's usually an explicitly agreed upon sequence, or perhaps the sequence "the n-th inaccessible"

[Mario Carneiro]

I guess it's not really that different from the choice constants though. At some point this sequence breaks down - it's well defined but no longer points at anything because you've run out of inaccessibles in the outer model, say - and you can do something similar with the choice sequence where you start with an assumption that gives you the first 42 choice constants and the rest of them are just nonsense

[Bas Spitters]

@Sebastien Gouezel lawvere set theory includes choice...

[Sebastien Gouezel]

Great!

[Mario Carneiro]

which choice?

[Bas Spitters]

https://ncatlab.org/nlab/show/ETCS
https://ncatlab.org/nlab/show/fully+formal+ETCS#the_theory_etcs

[Gaëtan Gilbert]

Mario Carneiro said:

I really sincerely don't understand why there isn't some reference linked from the coq manual or something that defines the whole axiomatic system and stays up to date with new versions

what about https://coq.inria.fr/distrib/current/refman/language/cic.html ?

[Gaëtan Gilbert]

Bas Spitters said:

Gaëtan Gilbert What is the status of strict sets?

I'm not working on them

[Assia Mahboubi]

Mario Carneiro said:

I really sincerely don't understand why there isn't some reference linked from the coq manual or something that defines the whole axiomatic system and stays up to date with new versions

I guess is related to the fact that the first released version of Coq is more than 30 years old. Nit-picking: other parts of a proof assistant, for which a paper description is seldom available, have at least as much impact on users and on their act of faith in formal statements. E.g. the elaborator, the parser etc. Since I am more interested in maths than in immediate applications in, e.g., security, I am not too worried though :).

[Mario Carneiro]

I am interested in specification for those aspects as well, but I think the logical foundation is the first stage, and in principle should be the easiest to obtain, being as well studied as it is

[Mario Carneiro]

@Gaëtan Gilbert That is a nice link. It is a bit tutorial-like though, and in particular the propensity to defer more complex aspects of the system until later makes it unclear when the description of the axioms is "done"

[Mario Carneiro]

I don't think you could write a Coq typechecker from that description

[Bas Spitters]

@Assia Mahboubi I'm interested in both math and security and that's why I think it's important that the logical foundations are well specified.
I believe the information is there for the Coq system, but they could be collected in a more central place.

[Mario Carneiro]

I am willing to believe that every piece of Coq foundations has been described in some paper written over the past 30 years. But there are also probably some bits of black magic in the ML code that never got air-time in a paper, and also the lack of central description means a lack of (proof of) global coherence, which is of course critical for soundness

[Bas Spitters]

@Assia Mahboubi Do you happen to know more about the parametricity plugin for lean and how it relates to classical logic?

[Mario Carneiro]

from the coq CIC manual:

the terms structurally smaller than $y$ are:

• $\mathsf{case}(c,P,f_1\dots f_n)$ when each $f_i$ is structurally smaller than $y$.

Isn't this the rule that caused a Coq soundness bug a while back?

[Mario Carneiro]

this one

[Mario Carneiro]

@Bas Spitters The parametricity plugin written by Cyril will prove the parametricity theorem for "any lean term". It works by recursion over the term syntax of the language, but it can get stuck when it gets to certain things. For axioms, there is nowhere to recurse so you have to manually provide a proof of parametricity. And choice simply doesn't satisfy the parametricity theorem, so any terms built using choice (and there are a lot of them) are similarly blocked. There are also complications in some inductive types, but last I saw there were no real theoretical barriers.

[Pierre-Marie Pédrot]

@Mario Carneiro Strictly speaking, this was not a soundness bug. It made Coq inconsistent with the standard Set model, which is indeed pretty bad, but doesn't allow to derive False either.

[Mario Carneiro]

I realize that another way to phrase this is "Coq is anti-classical", and that is what is done in the thread itself. But for all the lean users and mathematicians around here, that's basically just proving false things.

[Mario Carneiro]

Stated another way, it allows you to derive False in Coq + axioms that everyone wants to have and are unwilling to give up

[Bas Spitters]

@Mario Carneiro so, that approach to Transfer does not seem to be very suitable for lean...

[Mario Carneiro]

Right, somehow the pure "abstract nonsense" proof of parametricity doesn't work in practice because choice is too deeply ingrained. But for more engineering minded folks like myself the news isn't all bad. Although we use choice a lot to do proofs, it's not like we have choicy functions all over the place. Mathematicians by and large tend to avoid constructions that are not "canonical" in some sense and this means that "random functions" are quite rare. So one might hope to blockade the region around choice by proving, by alternate means, the parametricity theorem for certain terms that use choice in their definition, and then being able to stop the recursion when you get there rather than peeking into the definition and getting stuck on choice.

In particular, much of our usage of choice comes via classical.em, which I think satisfies the parametricity theorem because of proof irrelevance

[Pierre-Marie Pédrot]

@Mario Carneiro I am not sure what you refer to, but anti-classical has a well-defined meaning and this doesn't apply to Coq. Coq is compatible with classical logic, but it doesn't imply it. So, parametricity breaks in presence of classical logic, but that's not preventing the extension of Coq with classical principles. Furthermore, adding effects to a language just weakens parametricity, there are still weaker presentations that can be salvaged.

[Mario Carneiro]

When I talk about proving soundness of Coq, it may not be obvious but I don't mean "no axioms Coq", I mean "all common axioms Coq"

[Mario Carneiro]

I'm pretty sure there is a file in the coq standard library called Axioms.v or something like that containing a bunch of things commonly believed to be ok. I want those to all be consistent with Coq

[Pierre-Marie Pédrot]

This is ill-defined, people do use conflicting "common" axioms. Is UIP common? Is univalence common?

[Mario Carneiro]

If there are mutually incompatible supported subsets, they should be explicitly determined and the (probably quite distinct) proofs of consistency of each maximal consistent subset should be shown

[Mario Carneiro]

And also there should be GIANT WARNING FLAGS on these axioms to prevent someone from accidentally using both in the same development

[Pierre-Marie Pédrot]

This doesn't make sense, by Gödel's theorem there is no maximally consistent extension...

[Mario Carneiro]

The set of axioms in the coq standard library is finite

[Pierre-Marie Pédrot]

There is a nice graph somewhere in the doc, for set-theoretic axioms. Let me find it.

[Mario Carneiro]

I would have hoped that all the axioms taken together are consistent. Univalence is not in the coq standard library, I think

[Pierre-Marie Pédrot]

You can have a look at https://github.com/coq/coq/wiki/The-Logic-of-Coq and https://github.com/coq/coq/wiki/CoqAndAxioms.

[Mario Carneiro]

All 7 axioms on that page are consistent with each other in lean, and I hope in Coq as well

[Pierre-Marie Pédrot]

There is no such thing as "true mathematics" so it doesn't make sense to ask our users to abide to a specific set of axioms.

[Pierre-Marie Pédrot]

Compatibility is a strength. But if you like sets, you can throw in whatever set-theoretical axiom you fancy.

[Pierre-Marie Pédrot]

And I am not a crazy intuitionist, I would actually like to have some extension of CIC to classical reasoning that preserves its good computational properties. But it's far from being an easy task. And no, I don't consider that what Lean does is the right way.

[Mario Carneiro]

As long as the union of all provided axioms is still consistent, it's not so bad to work with subsets. You can choose not to use any of them, or just one, or just a different one, and all the libraries are compatible. As soon as you throw in an axiom that is inconsistent with the others, you bifurcate the libraries and the community

[Pierre-Marie Pédrot]

So what? There are people writing thread-safe code in C++, that doesn't mean that you can't also write code that is thread-unsafe.

[Mario Carneiro]

I actually don't particularly like lean's approach to axioms either. There are 3 axioms, and for almost all work you basically are forced to accept them all. There is very little room for playing with subsets

[Mario Carneiro]

In metamath there are something like 20-25 axioms, and while many of the subsets are not interesting, you can still play with avoiding the axiom of choice, or the axiom of foundation, or replacement, or first order logic, or intuitionistic logic.

[Mario Carneiro]

However, the union of all available axioms is TG set theory which is rather strong but still believed to be consistent

[Mario Carneiro]

so you don't need to have two separate libraries

[Pierre-Marie Pédrot]

This may look like an alien statement to the mathematicians around here, but I do think this kind of belief of "the one metatheory to rule them all" is 19th century thinking. If you accept proof-as-programs, then it makes sense to have several programming languages enforcing contradictory invariants. And this has nothing to do with the old feud between intuitionistic crackpots and the rest of the mathematical community, this is just about accepting the world as it is.

[Johan Commelin]

Who cares? If you want to get mathematicians on board, you'll have to accept that they don't care about foundations and just want to prove their theorems.

[Johan Commelin]

I know many mathematicians who really don't care about foundations. (I can't even list the axioms of ZFC myself.)

[Pierre-Marie Pédrot]

... or maybe we can teach the mathematicians about computer science to make them understand it's not a sterile debate?

[Mario Carneiro]

I'm all for supporting multiple foundations, but I also want to avoid erecting walls between formal developments

[Johan Commelin]

They don't care about correctness either. As long as proofs converge within a reasonable amount of time, that's fine.

[Mario Carneiro]

so compatibility is key

[Johan Commelin]

Pierre-Marie Pédrot said:

... or maybe we can teach the mathematicians about computer science to make them understand it's not a sterile debate?

They aren't interested in that either.

[Johan Commelin]

I don't say you should change. But in that case, don't get your hopes up on having mathematicians among your users.

[Pierre-Marie Pédrot]

@Mario Carneiro the situation is not as dire as you think from the point of view of foundations in the Coq community, there are mainly the Set people and the HoTT people.

[Johan Commelin]

What I am interested in is a proof assistant that helps me do research in arithmetic geometry.

[Johan Commelin]

Currently no such a thing exists.

[Pierre-Marie Pédrot]

@Mario Carneiro technical issues regarding the design choices of libraries are a much bigger issue than foundations.

[Johan Commelin]

And as long as I need to spend brain power on foundational issues, it won't happen either.

[Mario Carneiro]

Again, compatibility is key

[Mario Carneiro]

This is why mathlib is a monorepo

[Pierre-Marie Pédrot]

Once again, I think we should turn to programming engineering to draw inspiration. It is not uncommon to see various styles emerge. Then people tend to turn this state of affairs in the dreaded "platform" thingy so that you effectively get another programming language atop of the base one, enforcing more constraints like style and whatnot. If you need to make interact two libraries using different platforms, then you're toast.

[Mario Carneiro]

If it really is the Set people and the HoTT people, then asking mathematicians to use HoTT is like asking them to jump over the wall. And they very reasonably point out that they like the things on this side of the wall and don't want to give them up, even though there are some cool things on the other side too.

[Mario Carneiro]

At least there is the C ABI for interop when it comes to cross library compatibility in software

[Pierre-Marie Pédrot]

You can do Set theory in HoTT, but this is more like bondage than anything else.

[Pierre-Marie Pédrot]

As for C ABI, this is not a magical entity that happened overnight, this is the result of history and social interaction.

[Pierre-Marie Pédrot]

My personal belief is that MLTT plus or minus is a rather good minimal system.

[Mario Carneiro]

but you can't actually share results in a base theory, because the theorems need more than the base theory

[Pierre-Marie Pédrot]

There are French people believing that you should do everything via λΠ-modulo.

[Mario Carneiro]

If everyone worked in MLTT then they could be "universal donors" but there is no industrial strength implementation of MLTT

[Pierre-Marie Pédrot]

Well, so what? So be it. If I have code that uses threads, then it will break libraries relying on the absence of threads. That's life.

[Pierre-Marie Pédrot]

You don't consider Coq to implement MLTT, or that it's not industrial-strength?

[Johan Commelin]

@Pierre-Marie Pédrot Here is a result that I find extremely interesting: https://en.wikipedia.org/wiki/Resolution_of_singularities
I would like to know what you think is the shortest path to getting such a statement and proof in a computer proof assistent. I have all the reason to believe that Lean is currently the proof assistant that is moving in that direction the fastest.

[Mario Carneiro]

Coq implements a too strong theory, hence it cannot export results elsewhere

[Mario Carneiro]

The reason "Coq is a Lean typechecker" and not the other way around is because Coq is stronger. Strength is not a strength

[Pierre-Marie Pédrot]

@Johan Commelin foundation-wise, there is no real difference between Lean and Coq. Anything you can do with one, you can do with the other. @Mario Carneiro well, but nobody prevents you to define subsystems.

[Pierre-Marie Pédrot]

Coq is not stronger than Lean, @Gaëtan Gilbert had to specifically use unsafe features to implement Lean.

[Mario Carneiro]

It's very difficult to have subsystems of Coq where it matters. Can you turn off inductive types? Fancy pattern matches? Type n for n > 3?

[Pierre-Marie Pédrot]

If anything, modulo implemementation details, Lean is an extension of Coq.

[Pierre-Marie Pédrot]

What system do you want to get? As far as I am concerned, if you remove stuff like SProp, modules and template polymorphic inductive types, and only use eliminators, I get a reasonable foundation.

[Mario Carneiro]

The truth is that neither Coq or Lean is a subsystem of the other because DTT is too sensitive to minor differences

[Mario Carneiro]

Can I do something with equivalent axiomatic strength to HOL in Coq?

[Mario Carneiro]

Or at least not surpassing ZFC (without going intuitionistic / predicative)?

[Pierre-Marie Pédrot]

Coq is conjectured to be strictly weaker than ZFC + ω universes btw.

[Mario Carneiro]

you are talking no axioms coq though

[Pierre-Marie Pédrot]

At the risk of repeating myself, there is no such thing as "Coq + Axioms".

[Mario Carneiro]

I want all the axioms on that page

[Mario Carneiro]

Coq + those axioms

[Pierre-Marie Pédrot]

Yes, but then you get a crappy theory.

[Mario Carneiro]

Why? It's the theory mathematicians are used to

[Pierre-Marie Pédrot]

It's not a programming language anymore.

[Mario Carneiro]

or at least, the best approximation you can get to it within the constraints of dependent type theory

[Pierre-Marie Pédrot]

Having axioms in SProp does look like a promising way though.

[Mario Carneiro]

You know, I don't think saying "it's not a programming language anymore" will get you much sympathy around here. We don't want a programming language, we want a proof language

[Pierre-Marie Pédrot]

As for HOL, the Dedukti people wrote a few translators from various systems. You could try playing with it.

[Mario Carneiro]

You can always use computable things if you want to compute

[Pierre-Marie Pédrot]

This is why Coq has the distinction Prop / Type. Add you proof axioms in Prop, compute in Type.

[Mario Carneiro]

Sure, and none of those axioms interferes with this AFAIK

[Pierre-Marie Pédrot]

And FTR I don't really care about the sympathy of mathematicians. I have enough "real math" friends of mine who make fun of type theory and computer assistants. It's a social issue, not a technical one.

[Mario Carneiro]

I just don't see why they have to be at odds

[Pierre-Marie Pédrot]

Lean Santa Claus version of choice "inhabited A -> A" is very bad in the Prop / Type distinction though.

[Mario Carneiro]

Sure, it's noncomputable

[Mario Carneiro]

The cool thing is that if you use it only in proofs it becomes computable again

[Mario Carneiro]

that is, classical.em is computable

[Pierre-Marie Pédrot]

Well, breaking SR, strong normalization and whatnot.

[Pierre-Marie Pédrot]

I am afraid this is a dealbreaker.

[Pierre-Marie Pédrot]

But anyways, if a development uses choice, then will you consider this as valid?

[Mario Carneiro]

Axioms don't break SR, proof irrelevance and large elimination does

[Pierre-Marie Pédrot]

In a noncomputable way, I mean?

[Mario Carneiro]

strong normalization doesn't matter

[Pierre-Marie Pédrot]

(You can't shift the blame one one axiom, it's the whole interaction of rules.)

[Mario Carneiro]

That concerns the behavior of #reduce which we literally never use because it's impractically slow on almost all examples

[Pierre-Marie Pédrot]

strong normalization doesn't matter

[Pierre-Marie Pédrot]

for some people it does

[Pierre-Marie Pédrot]

so, please answer the question: assuming some subcommunity wants to restrict to computable functions

[Pierre-Marie Pédrot]

for some reason, doesn't matter

[Pierre-Marie Pédrot]

what does mathlib tell them?

[Mario Carneiro]

What matters is evaluating computable functions that were written to be computable, not evaluating all terms anywhere in the proof assistant including proofs and stuff

[Pierre-Marie Pédrot]

OK, this foundation stuff is a red herring. Let me put it another way. Assume there are people deciding to go ssr-style in Lean.

[Pierre-Marie Pédrot]

What happens? A fork?

[Pierre-Marie Pédrot]

That's essentially what happened to Coq a long time ago.

[Mario Carneiro]

Lean has a marker, called noncomputable, that you are required to put on any definition that cannot be executed. There is a way to put this at the start of your file to say "I don't care about computability", and most mathematicians do this for their theories of category theory, commutative algebra and whatnot. If you care about computability, you write computable defs, which don't have this marking, and lean will generate bytecode on the spot. These functions can be called via #eval with concrete arguments and you get values out just like any programming language.

[Pierre-Marie Pédrot]

Right, right. But my point is about the existence of diverging design choices in library in software.

[Pierre-Marie Pédrot]

Doesn't even have to be Lean.

[Mario Carneiro]

Moreover, there are ways to compute even with noncomputable terms, using tactics, and this is in fact the preferred method (by comparison to proofs by reflection). This is exemplified in tactics like norm_num that will prove things like 100 + 100 = 200 by cobbling proofs together, even though yes, you could prove it by rfl, the proof takes too long

[Pierre-Marie Pédrot]

Invariably, there will be people disagreeing with whatever choice done in mathlib.

[Pierre-Marie Pédrot]

the proof takes too long

really? this sounds suspicious to me

[Mario Carneiro]

It unfolds into unary. It's bad

[Pierre-Marie Pédrot]

yes, but tactics will have to generate similarly big proof terms

[Pierre-Marie Pédrot]

doesn't it mean that the reduction machine is not really optimized in Lean?

[Mario Carneiro]

The short story is that in Lean the tactics are fast and the kernel reduction (plus elaborator reduction) is comparatively slow. In Coq it is the other way around and the cost benefit analysis goes the other way

[Pierre-Marie Pédrot]

OK, this is surprising.

[Mario Carneiro]

Checking big proof terms is not that bad, as long as the types all line up

[Pierre-Marie Pédrot]

well, type-checking is at least linear in the size of the term

[Mario Carneiro]

yes, that's fast if the term is small

[Pierre-Marie Pédrot]

yeah but I fail to see how you can build a reasonable proof of "100 + 100 = 200" that is not generating a term requiring more work than mere evaluation, in unary that is

[Mario Carneiro]

Note also that if you provide a proof term you have a lot of flexibility in how to do the computation. For example when norm_num proves or disproves primality, the first thing it does is find out if the number is actually prime, and if not, it has a very short proof of the negation. A reduction based proof would have to do the whole primality thing even in the composite case

[Pierre-Marie Pédrot]

depends how you write it

[Mario Carneiro]

You can produce a proof of 100 + 100 = 200 in size linear in the size of the expression, which is written in binary after the parser has had a go

[Pierre-Marie Pédrot]

the ssr people are very good at this kind of stuff

[Reid Barton]

The literal "100" itself is not in unary, as a term

[Bas Spitters]

@Mario Carneiro @Johan Commelin Is it possible that what mathematicians in lean are really using is Lawvere's version of choice as in ECTS, and not Hilbert epsilon which is non-structural.

[Mario Carneiro]

Let's suppose you want to reduce prime N to true or false where N is some big number, say 50 digits. You have no choice but to push the kernel through a bunch of states to test the primality, while a tactic can just call GMP or mathematica to first factorize it and then prove the correctness of this untrusted guess

[Pierre-Marie Pédrot]

@Mario Carneiro that's assuming you go full reflection, but precisely the ssr people are argueing for interleaved computation with tactics.

[Mario Carneiro]

Is that so? I didn't realize that. I usually have a tough time being able to insert a proof term in the middle of a defeq computation

[Pierre-Marie Pédrot]

I am probably not qualified enough to talk about this but this is precisely the whole story of the "small-scale" nature of this approach. I'd recommend asking @Assia Mahboubi for instance.

[Mario Carneiro]

@Bas Spitters In a literal sense, of course they are not; lean provides one choice axiom and they are using it. But more likely you mean that they would be equally happy with a Lawvere style axiom of choice, and I'm not sure this is true. Among other things, we use choice to do definite descriptions. So things like sum (f : nat -> real) : real will be defined using choice. (It would also be used here to do an outer if statement: if the sum is not defined then return 0 else return the unique sum of the sequence.)

[Reid Barton]

I think this "naked choice" is potentially problematic even just in the context of Lean itself. For example (as noted earlier, I think) it blocks automatic syntax-directed proofs of parametricity.

[Reid Barton]

It would be better to split off axiom_of_choice (the Prop version) and unique_choice into separate axioms

[Bas Spitters]

@Johan Commelin I am not an expert on this topic, but the people in constructive/computer algebra have considered this topic. E.g.
https://arxiv.org/abs/1304.6770
What is interesting is that the same abstractions are useful in topos theory (Coste, Roy, Lombardi, Wraith, ...) and in computer algebra (magma,GAP, ...)
@Assia Mahboubi may know more.
I would imagine that a more algebraic development is more suitable for formalization. However, it is possible that we do not have all the right abstractions yet.

[Reid Barton]

Then some definitions like (hypothetically, I don't think this is the actual mathlib definition) the dimension of a vector space as "pick a basis, and take its cardinality" can be formulated in terms of unique_choice, but it requires proving that the result is independent of the choice. Which is also the rule in ordinary math.

[Reid Barton]

(I think the actual mathlib definition is "the smallest cardinality of a basis"? but surely there are other examples)

[Mario Carneiro]

sum mentioned above is an example. There are two uses of choice in that definition, and they are both definite descriptions

[Gabriel Ebner]

I'm not sure how the dimension of a (real) vector space could ever be computable. What is the dimension of the span of a real number x? This requires computing whether x is nonzero. But alas, that's noncomutable.

[Mario Carneiro]

It's not computable, unique_choice would still be an axiom

[Gabriel Ebner]

Ah, sorry didn't follow the discussion too much. unique_choice [subsingleton A] : nonempty A -> A then?

[Reid Barton]

This also fits better with my mental model of the semantics--I want to say you get a model of Lean from a model of ZFC+omega inaccessibles, not from such a model together with some specific choice of choice functions.

[Reid Barton]

Of course full choice would probably be needed/convenient for some purposes, but at least you could track it separately

[Mario Carneiro]

You can also do unique_choice : unique A -> A

[Gabriel Ebner]

This version of unique_choice doesn't require an axiom though, since unique extends inhabited.

[Mario Carneiro]

oh

[Mario Carneiro]

nonempty (unique A) -> A? Doesn't have the same ring

[Bas Spitters]

Corollary 3.9.2 (The principle of unique choice). Suppose a type family P : A → U such that
(i) For each x, the type P(x ) is a mere proposition, and
(ii) For each x we have || P( x)||.
Then we have ∏( x:A ) P( x).

[Mario Carneiro]

The use of a type family there seems superfluous

[Mario Carneiro]

Note that lean's choice used to be more complicated, and it was simplified to the current nonempty A -> A

[Mario Carneiro]

I think the original axiom was indefinite_description {α : Sort u} (p : α → Prop) : (∃ x, p x) → {x // p x}

[Mario Carneiro]

If I ignore the thing about the type family (set A = unit), then it seems that the HoTT version reduces to what Gabriel posted

[Gabriel Ebner]

The Lean version of unique choice is pretty strong since we have more subsingletons, e.g. it implies that all types have decidable equality. Does the HoTT version allow you to write λ x : ℝ, if x = 0 then tt else ff?

[Bas Spitters]

@Gabriel Ebner I believe so in the presence of PEM. Since the term is definable in ECTS using unique choice.

[Mario Carneiro]

I think the proof of unique choice in HoTT is similar to the lean proof of [subsingleton A] : trunc A -> A

[Kevin Buzzard]

Pierre-Marie Pédrot said:

There is no such thing as "true mathematics" so it doesn't make sense to ask our users to abide to a specific set of axioms.

@Pierre-Marie Pédrot in my department the vast majority of us think ZFC is true mathematics, and I am certain that many other mathematics departments think the same way. The fact that logicians and computer scientists have invented a whole bunch more options and then decide to call them mathematics is problematic, because it means that discussions can degenerate into axiomatic issues which as far as a mathematician is concerned are completely solved. The axiom of choice is an axiom of maths as practiced in mathematics departments. Johan is absolutely right when he says that mathematicians are not interested in this stuff. You say

... or maybe we can teach the mathematicians about computer science to make them understand it's not a sterile debate?

but it is much worse than that -- it is not a sterile debate -- we finished debating 100 years ago and decided what mathematics was, and the fact that you guys are still arguing over it is of no interest to us. From your point of view this debate is very important, because if you want to design a new computer proof system than of course foundations are absolutely a major issue. But from a mathematician's point of view, ZFC works, constructivism doesn't work, ZF doesn't work, and these topics are not being studied in mathematics departments other than by a small niche group of people. We mathematicians are looking for a system where we can reason the way we reason on paper and having tried several systems I currently believe that Lean 3 is the closest we have to this; I can name explicit problems with every other system, either of the form "not enough foundations yet" or "can't do some part of modern mathematics in a way which is practical". For Coq it is "quotients", which are absolutely everywhere in modern mathematics.

Once again, I think we should turn to programming engineering to draw inspiration.

We mathematicians cannot turn to programming languages to draw inspiration because for you guys it's really important to have lots of different programming languages, because different languages are good at different things. We are attempting to make one coherent body of mathematics, and it's really important that everything is compatible with everything else. In particular every paper in number theory has to be accessible to me if I am a number theorist so it's really important that they all have the same foundations, and these foundations are decided -- they are ZFC -- and sure, add universes if you like, it doesn't matter, because it turns out that the kind of mathematics we do can sometimes be made easier with universes but we actually know tricks to get it back into ZFC. But we will not settle for anything less. LEM and AC are embedded. We are not going back.

And FTR I don't really care about the sympathy of mathematicians. I have enough "real math" friends of mine who make fun of type theory and computer assistants. It's a social issue, not a technical one.

What I am trying to do in Lean is to bring mathematicians in and get them using this software. In particular I need to hide type theory if I want to get them to use computer assistants. It is a social issue and it is one which I think is extremely important, but we as proof assistant users need to tread carefully when attracting mathematicians into the area. I simply tell mathematicians that a type is a set where the elements aren't necessarily sets any more but could just be "atoms", and suggest that actually this is the way they think about stuff they call sets.

I want to meet computer scientists "half way" and so I can have some dialogue with them about the future of these sytems -- but there are some ground rules, and AC and LEM and noncomputability are part of them. Any suggestion that a system which doesn't have them can be used to do modern mathematics is ridiculous to our ears, so the conversation cannot even start. This is why I use Lean and this is why I tell other mathematicians to use Lean.

[Pierre-Marie Pédrot]

LEM and AC are embedded. We are not going back.

This is great, because that's what some people in the community are trying to provide in type theory in a way that actually works. Disclaimer: I am one of those, and I am not advocating against EM + AC. I am just constantly disappointed by the lack of consideration from mathematicians on the topic of foundations. And I am not saying that anybody should turn into a type theorist, but at least that they should be listened to, which is very different.

So far, the logical choices of Lean are the dependent type theory equivalent of PHP. Yes, it kind of works, until you reach the size of Facebook and realize that you wrote your stuff on quicksand, and that disregard for foundational issues have a long term cost you'll only realize at that point. And now, they're switching parts of their code to ReasonML because the trade-off is long overdue.

What I am trying to do in Lean is to bring mathematicians in and get them using this software.

I am not complaining about that. It is better to use whatever proof assistant than nothing, and the state of a few areas of mathematics is depressing. Needing a Fields medal to dismiss a broken proof is not a great situation, if you ask me.

What I am trying to do in Lean is to bring mathematicians in and get them using this software. In particular I need to hide type theory if I want to get them to use computer assistants. [...] actually this is the way they think about stuff they call sets.

There is wide evidence that no mathematician ever uses ZFC anyways, so I don't think it's very hard to make them forget about sets, except maybe for some weird hilbertian fetichism.

For Coq it is "quotients", which are absolutely everywhere in modern mathematics.

I will call your bluff, because you keep spreading this lie around, and I am starting to be slightly annoyed. As demonstrated by @Gaëtan Gilbert , it is perfectly possible to get quotients in Coq with the very same rules, if you opt-in for a broken feature that is hardwired in Lean. Even Santa Claus choice can be obtained by similar tricks. I have actually heard rumours that you didn't even try Coq thoroughly, and I even believe there is a written account of that. You don't have indeed to try everything out there to settle for a tool, and it's nice to see math users playing around with any type-theoretic proof assistant.

Yet, I am a type theorist and I would never not making random claims in some arbitrary area of mathematics.

But once again, I claim the minimal divergence of foundations between Lean and Coq are of little relevance to formalization of mathematics. From what I gather, Lean has not reached Gonthier's famous wall of complexity. By that, he means that a lot of a priori ridiculous technical impediments are paving the way to mathematical formalization. I am genuinely willing to see an actual large mathematical development in Lean, to satisfy my own computer scientist fetichism, namely scalability. It might be changing, but Coq proofs are still a cottage industry. Can Lean do better?

[Sebastien Gouezel]

Pierre-Marie Pédrot said:

As demonstrated by Gaëtan Gilbert , it is perfectly possible to get quotients in Coq with the very same rules, if you opt-in for a broken feature that is hardwired in Lean. Even Santa Claus choice can be obtained by similar tricks.

I don't think the question is whether they can be constructed in Coq. To an outsider to type theory like me, the systems are sufficiently similar that I have little doubt that something natural that can be made with one can be made with the other. The question is rather whether they are used in the libraries, i.e., if the main libraries with the software try to use a constructivist point of view, or don't care and go full classical right away. Here I can see a really different approach currently with the Coq and Lean communities. I think it is very healthy that different viewpoints are tried and put forward, but mathematicians will be more easily attracted to libraries that use choice and LEM from the very beginning, because it will sound more familiar to them.

[Kevin Buzzard]

You are right about my Coq experience. I heard about this "setoid hell" from various people but I am certainly not an experienced Coq user. I will try and get some more concrete facts.

Mathematicians are terrible about foundations. It is not regarded as an interesting topic by most people, because "all the interesting questions were solved when forcing was invented" or something :-/ You are also right that we don't use ZFC in practice, however it is true that there is a general belief that whatever it is that we are doing, it is possible to translate it down to ZFC (and classical logic) in theory. My impression is that in the areas I am interested in (number theory, arithmetic geometry) it is possible to find people (they are rare, but they exist) who actually know how to do this, but it is not something which is deemed particularly important. Somehow the workers in each area know the API, and then a few people know how to get from the API to the foundations, but what is taught is the API.

I am not necessarily saying that Lean is the solution to everything. But I think it is close enough to being able to simulate the kind of mathematics done by mathematicians that it might be enough to get people interested in the theory in general. My general line of thought is this. Which system is best for modern mathematics? We don't really know. So let's try and get mathematicians actually making mathematics in as many systems as possible, because my impression is that when we get stuck the computer scientists are able to understand what the problem is and try to solve it. You know we have some typeclass problems in Lean 3, which I think were basically discovered because of mathematicians trying to push the system? Hopefully these will be fixed in Lean 4.

I guess it will take time before we have a large development. I guess we are working on mathlib as being this development?

[Pierre-Marie Pédrot]

mathematicians will be more easily attracted to libraries that use choice and LEM from the very beginning, because it will sound more familiar to them.

I don't know why Coq has this aura of knife-between-their-teeth intuitionists in the mathematical community. Just as mathematicians, most computer scientists don't care at all about their foundations. Most serious computer science Coq developments I know of actually use classical axioms everywhere.

[Kenny Lau]

Is knife-between-their-teeth a French phrase?

[Kevin Buzzard]

It's clear what is meant :-)

[Kenny Lau]

I actually wasn't able to infer it from context

[Kevin Buzzard]

I remember one of the first things I noticed when reading the Coq odd order paper was that they said that the result was proved constructively, and I thought "what does that even _mean_?" (this was a few years ago before I knew the definition). And then later on they started explaining about how they couldn't use the complex numbers and I was totally speechless. I think it is more the issue that constructivism is simply not taught in mathematics departments, so we find anyone who talks about it slightly scary.

[Kevin Buzzard]

I literally had no idea 5 years ago that the complex numbers were somehow illegal for some people.

[Pierre-Marie Pédrot]

It's strange, because I am fairly sure mathcomp uses classical logic locally. Dually to Lean, they mark classical statements by quantifying over a proof of EM. Anyway, AFAIR it does not even matter for the odd order theorem since it's a negative statement, which are essentially equivalent in intuitionistic and classical logic.

[Kevin Buzzard]

I guess the point is that all the constructions they used in the proof were also constructive.

[Pierre-Marie Pédrot]

See Chapter 3.3 of https://math-comp.github.io/mcb/book.pdf.

[Sebastien Gouezel]

When I started with proof assistants (I wanted to do some measure theory), I tried both Coq and Isabelle and I gave up very quickly with Coq, one of the reasons being that in the standard library many files talking about the reals start with the word "Constructive".

[Kevin Buzzard]

The link is just the sort of thing that mathematicians find intimidating. We do not teach decidability in any serious way; I think I met it once in the 2nd year logic course and then it was never mentioned again (and I am certain that my 3rd year lecturers did not know what it was). I learnt very quickly when talking to mathematicians about Lean that the moment you start mentioning these things they think you've become some kind of crank.

[Kevin Buzzard]

I think this is the main reason I am so edgy about the univalence axiom. It starts with a discussion of univalence, and within minutes the conversation has either turned to elementary topoi (about which mathematicians know nothing), or constructivism (about which mathematicians know nothing), or some discussion about how things can be equal in more than one way (which just sounds like complete craziness). It is so far from what happens in practice in maths departments.

[Pierre-Marie Pédrot]

many files talking about the reals start with the word "Constructive"

This is funny because precisely the Coq real library from stdlib is classical, to please the mathematicians. I guess merely uttering the word "constructive" is enough to deter mathematicians then...

[Sebastien Gouezel]

Absolutely. Because it means, at some point, you will have to make some effort to stay constructive (otherwise, you wouldn't put the word constructive in the file name). So, the definition starts with some constructive stuff, and then goes classical. To me, if you can express a statement or a proof by remaining constructive but it requires 1% effort more, then it should be avoided (both for the library builder, and for the user who will have to skim the library), simply because there's no point. Maybe I am a little extreme there, but I think it is pretty reasonable in fact.

[Johan Commelin]

On this forum, I can say that I see value of constructive maths (for example, constructive maths holds in any topos). But when I'm having lunch with my colleagues, they don't want to hear anything about giving up the C in ZFC. So yes:

I guess merely uttering the word "constructive" is enough to deter mathematicians then...

My goal is to get them engaged with proof assistants. And for that, mentioning the word "constructive" is quite often an unfortunate obstacle.

[Pierre-Marie Pédrot]

@Sebastien Gouezel well, until very recently Coq reals were fully axiomatic, so there was not even a hint of constructivism in there. Now they're trying to have some subsystem that's constructive in order to plug into C-CoRN.

[Bas Spitters]

Georges seem to take it as a matter of pride to make a constructive proof. Georges has a deep appreciation for the use of computation to proof mathematical theorems.

[Kevin Buzzard]

I am wondering whether the mathlib people take pride in the fact that the development is 100% axiom-free. Sure we use Lean's inbuilt axioms (because this is just "maths mode") but there are no instances where we build a mathematical object by just adding axioms.

[Pierre-Marie Pédrot]

Somewhat unrelated to the discussion, but @Sebastien Gouezel we could try to have more discussions on the topic in person, we're just one building away IIUC... (when they reopen the uni, that is.)

[Bas Spitters]

There is now a substantial development of constructive measure theory in Coq. Following Bishop, who was a great functional analyst.
https://github.com/coq/coq/pull/9185
The classical theorems are then derived quickly from the constructive ones. One does not need to do it that way, but some people appreciate it.

[Pierre-Marie Pédrot]

they don't want to hear anything about giving up the C in ZFC.

One of the advantages of type theory is that they are finer-grained than sets, and that it's easier to understand what is what. The usual joke on the understandability of choice vs. Zorn vs. well-ordering makes sense there. CIC validates choice phrased as "you can pick elements of existentials".

[Sebastien Gouezel]

Pierre-Marie Pédrot said:

Somewhat unrelated to the discussion, but Sebastien Gouezel we could try to have more discussions on the topic in person, we're just one building away IIUC... (when they reopen the uni, that is.)

Definitely! In May or June, maybe :-)

[Johan Commelin]

Pierre-Marie Pédrot said:

One of the advantages of type theory is that they are finer-grained than sets, and that it's easier to understand what is what. The usual joke on the understandability of choice vs. Zorn vs. well-ordering makes sense there. CIC validates choice phrased as "you can pick elements of existentials".

That's a good point. Thanks for pointing it out! Still, it's only useful for mathematicians if you can also have transport (not only along equiv's, but also other isos) and have a sizable library of "basic maths".

[Bas Spitters]

@Johan Commelin Peter Johnstone once wrote an apology for locale theory, and the benefits of working classically, but without choice.
The point of pointless topology
https://projecteuclid.org/euclid.bams/1183550014
Choice is only used to construct the points of a locale. The locale it self can be constructed without choice. The use of the axiom of choice is a choice.
This has applications in e.g. functional analysis.

[Bas Spitters]

@Sebastien Gouezel I had a quick look at your homepage.
https://www.math.sciences.univ-nantes.fr/~gouezel/
You seem to be working in a beautiful part of analysis that is not very structural, i.e. somewhat distanced from say functional analysis.
Moreover, does not seem to be very computational/numerical.
So, constructive methods may be less natural to you.

[Patrick Massot]

:open_mouth: I think this is the first I see anyone claiming to know which part of mathematics Sébastien works in.

[Bas Spitters]

About the Hausdorff metric. My PhD-student once used it to make a 1980-style graphical calculator which was provably correct. The printing of graphs of functions was done using the Coq notation system.
https://www3.risc.jku.at/publications/download/risc_3448/SCSS2008_Proceedings.pdf
Russell O’Connor. A Computer Verified Theory of Compact Sets. SCSS 2008, RISC-Linz Report Series 08–08: 148–162, Jul 2008, Proceedings

[Sebastien Gouezel]

I use a lot of functional analysis (in the sense of operator theory on spaces of functions, so with concrete applications to other problems in mind), but not on the abstract side of things (I know what a trace on a C^* algebra is, but I don't use them in my research). So, I am away from the finite world (where decidable methods are appealing because they can let you compute for free on examples), and away from the more abstract sides (higher homotopy theory for instance) where foundational discussions become relevant. So yes, I am definitely biased away from these questions. But I guess that this is also the case of maybe 90% working mathematicians.

[Bas Spitters]

While I'm at it. One can use constructive analysis to do certified computation with classical real numbers:
Cezary Kaliszyk and Russell O’Connor. Computing with Classical Real Numbers. Journal of Formalized Reasoning, Vol. 2, No. 1, 2009, Pages 27–29
http://jfr.cib.unibo.it/article/view/1411/932

How does one prove in lean that:
pi ~ 3.14159265359 ?

[Johan Commelin]

We can only do the first 4 digits (-;

[Johan Commelin]

Maybe we pushed till 7 digits, on last years Pi-day

[Bas Spitters]

@Johan Commelin So, that's one reason you should have used constructive reals :-)

[Johan Commelin]

Or we just need some tactic that can spit out proofs.

[Bas Spitters]

Arguably, one can also connect with interval computation "by hand", as in the impressive work by Fabian Immler in Isabelle to prove that the Lorentz attractor is chaotic

[Patrick Massot]

I really don't understand that bit. Say I prove some series $\sum a_n$ of rational numbers converges to pi. I can do this 100% classically. And then I prove an estimate on the remainder $\sum_{n\geq N} a_n$. Then I can prove the first $k$ digits are correct. Where do I need anything constructive as long as I can prove all this and compute with rational numbers?

[Bas Spitters]

For most of basic analysis such proofs would be naturally constructive, and one would combine the proof of convergence with the estimate on the remainder.
You are right, it is not needed to do so.

[Sebastien Gouezel]

In Isabelle, which is completely non-constructive but more mature, you would prove it with

lemma ineq3:
  "(pi :: real) ≤ 3.141592658"
by (approximation 40)

where approximation is a tactic that will do all the dirty interval arithmetic for you.

[Chris Hughes]

So my understanding is that if I had a constructive proof of convergence of $\sum a_n$, then given some $\epsilon$ I could compute $N$, such that the sum of the first $N$ terms was within $\epsilon$. But the problem with this is that it means whenever I do a continuity proof or a convergence proof I will have to think about providing a minimal $\delta$ or a minimal $N$, in order to make sure the computation time was reasonable, but often with the standard proofs, you'll end up computing an $N$ way bigger than it really needs to be and not really practical to compute with.

Does an unfolded proof of convergence actually provide a practical way of approximating the limit most of the time?

[Bas Spitters]

@Sebastien Gouezel Coq has a similar package:
http://coq-interval.gforge.inria.fr/

[Sebastien Gouezel]

Yes I am not surprised: Coq and Isabelle are much more mature than Lean, so most things that should be there are already there.

[Bas Spitters]

@Chris Hughes With a bit of engineering this can be made practical. However, with epsilon-delta proofs one is computing backwards from the precision of the result to the precision of the input.
For optimal speed, one wants to compute forwards: start with a small interval see whether the result is precise enough. If not, start over with double precision. This is what IRRAM does:
https://github.com/norbert-mueller/iRRAM
I believe mathematica does something similar.

[Bas Spitters]

Hoping I wasn't too zealous, I just wanted to point out that constructive mathematics has its uses in the formalization of mathematics, even if one is not a diehard constructivist.