Make mathlib less dependent on choice

Stream: general

[Riccardo Brasca]

Dear all,
For various reasons, I recently became interested in trying to make mathlib a little less dependent on the axiom of choice.

Using the script written by @Paul Lezeau and @Robin Arnez here we know that 387254 declarations in mathlib (including various dependencies) use choice, this is roughly 55% of the total declarations.

Of course, there are genuine mathematical reasons to use choice, and avoiding it is in general a difficult problem (likely open for many advanced results, and certainly nontrivial even on paper). On the other hand, mathlib contains many declarations where avoiding choice is mathematically trivial. One example (the first one I encountered in practice) is Fin.fintype, which you can check depends on Classical.choice.

My current idea is to eliminate uses of choice in such mathematically trivial situations. This is therefore unrelated to the broader question "Is there a choice-free proof of X?" More precisely, I am only interested in those X for which the answer is clearly yes.

An important point is that I am not proposing to modify mathlib itself, but rather to maintain a parallel version that depends less on choice, with a minimal diff. I have started working in this direction in #35027, where I remove choice from Fin.fintype. As you can see, the diff is relatively small (about 60 lines correspond to the script mentioned above), and in practice it mainly consists of removing uses of grind in very basic lemmas about lists. This already results in more than 200 declarations no longer depending on choice.

I would be interested in hearing opinions about such a project, especially whether others might be interested in contributing. At the moment, I think maintaining this as a PR is the most convenient way to proceed: it allows people to inspect the diff and also provides the cache. If you look at the PR, you will see that some lemmas that use choice live in core, so I cannot modify them directly in a mathlib PR. Instead, I have reproved them in a separate namespace. If anyone has a better idea for handling this, I would be very happy to hear suggestions.

Also, I don’t have a coherent roadmap. At the moment I’m proceeding opportunistically, removing uses of choice in lemmas that arise in another project where I’m trying to stay choice-free (for example I currently need a choice-free version of Finset.powerset).

[Chris Henson]

Could this sort of work be in a repo with Mathlib as a dependency that is focused on reproving things without choice? I'm imagining a command elaborator like theorem, but that is used to register a choice-free equivalent of an existing declaration. Maybe it could solve the awkwardness of choice in core by registering these in a way that can be referenced in the metaprogram for checking dependency on choice.

[Riccardo Brasca]

I have no idea if this is doable with metaprogramming (it would be very nice!). The important point is that a modification to declaration X should propagate to all declarations depending on X.

[Riccardo Brasca]

And with my current approach this happens in mathlib, but not in core. I am not familiar with how to modify core (and having cache for mathlib), this is why I choose this suboptimal approach.

[Michael Rothgang]

I'm curious about your motivation for this project :-)

[Riccardo Brasca]

I started because I wanted to formalize a bit of Synthetic differential geometry. This happens in a topos, so one can work in the internal logic, i.e. forgetting about toposes and pretending to be in the usual world of mathematics, but without excluded middle, so without choice in Lean (for my project I added the axiom of unique choice, but this is another story). At first I just wanted to see what happens with mathlib, since we use classical reasoning freely.

[Riccardo Brasca]

I was quite surprised that things went reasonably well even with powerful tactics (for example ring works like a charm). The first issue I encountered was the ridiculous use of choice in writing (2 : R), see #32467. Then I had to manipulate various sums over Fin and there things were not so nice.

[Riccardo Brasca]

But I realized that very often the use of choice could be tracked back to a single grind line in a very trivial result, and that the ratio (number of lines to modify)/(number of theorems that become choice free) can, at least at the beginning, be very very small. This why I had the idea of starting doing this. Note that currently, if I could modify core, the diff would be only 5 or 6 lines, and there are 435 theorems that become sorry free (and if the modification would be actually in core this number would probably be considerably higher).

[Riccardo Brasca]

@Michael Rothgang am I correct in saying that you asked here how to modify core in such a way to have cache in mathlib depending on the new version? Is the guide reliable now?

[Michael Rothgang]

I wasn't asking about having mathlib cache per se, but that might have been implied by it. I didn't have the chance to come back to the thread yet, so I don't know if the instructions are fully up-to-date now.

[Snir Broshi]

I think trying to avoid choice/LEM sometimes creates proofs that are easier to follow (similar to how apply foo; ... is easier to follow than have := ...; exact foo this), and such improvements should make their way into main Mathlib.

[Snir Broshi]

How about a project to replace most usages of Quot.out/Quotient.out with induction/recursion? This is a use of choice that is generally frowned upon. It won't necessarily make stuff avoid choice entirely, but it seems aligned with the general goal.

[Riccardo Brasca]

It's very difficult to guess where choice is used. Of course there are results that surely depend on choice, but in practice I think it's much more efficient to target extremely basic declaration, at least at the beginning. You may replace Quotient.out by induction and discover that your theorem still depends on choice for ridiculous reasons. If you think using induction could improve readability of a proof you can actually open a PR to mathlib, it is a welcome contribution.

[François G. Dorais]

@Riccardo Brasca, have you tried cutting some non-essential uses at the stem? Many uses of Classical.choice rely only on some theorems like Classical.em. Making the latter an axiom and removing the theorem should already drastically reduce the uses of Classical.choice.

There is a hierarchy here:

• Classical.em basically just means that the metatheory of Lean is classical. This is very mild and most mathematicians are happy with a classical metatheory.

• Classical.propDecidable is stronger, it says that the internal logic of Lean is classical. For example, this means that every Type u is a Boolean topos from the category theory point of view.

• Classical.choice is strongest but it is the status quo.

(There are of course several intermediate steps but they are not so important for now.)

[Riccardo Brasca]

Well, my mathematical goal is exactly to avoid excluded middle, so in practice this means avoiding choice in Lean.

[François G. Dorais]

Classical.em or Classical.propDecidable?

[Riccardo Brasca]

But currently my question is rather what is the best way of doing this from a practical point of view. It's more a software engineering problem than a mathematical question.

[Riccardo Brasca]

I want to avoid Classical.em.

[François G. Dorais]

Why do you need an intuitionistic metatheory? That is very rare.

[Riccardo Brasca]

Honestly I don't know anything about this, so it's possible I am saying nonsense. But if I understand correctly the internal logic of a topos is an intuitionistic theory, and I started formalizing synthetic differential geometry in Lean, working internally. Of course the metatheorem that says I can work internally "as I do usual mathematics, but I cannot use excluded middle" is not in Lean, but I am just pretending it is. I apologize if what I am saying is imprecise/nonsensical.

[Riccardo Brasca]

This raised the very practical question of proving theorems using mathlib in such a way that #print axioms foo does not display Classical.choice, and I ended up doing so essentially because I am curious about how far I can go.

[Riccardo Brasca]

Let me stress again that mathematically what I am doing is completely trivial. I am talking about modifications like those in lean4#12635. Now these declarations don't depend on choice anymore, and this gives like 400 less declarations in mathlib that use choice. It's much easier than actually asking "is there an intuitionistic proof of this not so trivial theorem?"

[François G. Dorais]

Classical.em doesn't prevent Type u to be internally intuitionistic. It mostly means that you're using classical logic to reason about Type u. There are a few small consequences to this, such as Markov's Prinicple, ∀ (p : Nat → Bool), ¬(∀ n, p n) → (∃ n, p n), which is provable using Classical.em.

Several automation tools could just run on Classical.em, so your project could be progressive: eliminate Classical.choice but keep Classical.propDecidable, then eliminate Classical.propDecidable but keep Classical.em, then eliminate Classical.em.

[Riccardo Brasca]

I don't see how to actually check something does not depend on Classical.em. Note in Lean it is not an axiom, it is proved using Classical.choice, so if a declaration does not depend on choice than that's ok, but on the other hand it's difficult to say "X uses Classical.em but not full choice".

[Riccardo Brasca]

The same for the others Classical.foo. The only actual axiom is choice.

[Edward van de Meent]

you can probably (try to) transitively inspect theorems to see if Classical.em is part of the proof bodies?

[Edward van de Meent]

since i don't believe inlining the proof that Classical.em follows from Classical.choice is allowed with mathlib's style guide

[Chris Henson]

Yes, the linked metaprogram for choice collects constants, right? I don't think it is specific to axioms.

[Riccardo Brasca]

Maybe, but that's quite orthogonal to what I want to do. I am sure my theorem has an intuitionistic proof (it seems clear to me, and this is people working synthetic differential geometry, or related area, are expert in noticing uses of classical reasoning). What I am less sure about is if I can actually prove it using mathlib.

[Riccardo Brasca]

Chris Henson said:

Yes, the linked metaprogram for choice collects constants, right? I don't think it is specific to axioms.

It's better to ask the authors since I basically know nothing about metaprogramming, but this is my impression too.

[François G. Dorais]

Make a draft PR to core changing Classical.em to an axiom. That will create a PR testing toolchain and a mathlib-testing branch that you can play with at will.

[Ruben Van de Velde]

But what's the point?

[Riccardo Brasca]

I am still trying to understand how all the process of creating a toolchain etc etc works, so give me some days to play with lean4#12635 :)

[Riccardo Brasca]

For example I see that now there is a toolchain, but I think to mathlib PR (I rebased onto nightly-with-mathlib but nothing happened).

[Riccardo Brasca]

ah, now there is a mathlib available, so it was just a matter of time

[J. J. Issai (project started by GRP)]

Ruben Van de Velde said:

But what's the point?

The point is to refine what is actually needed for a result (in which topoi or models, say, a result can live). This should have implications not just for reverse mathematics but for future versions where Mathlib splinters into the versions needed for people working in various systems.

Making one Mathlib for formalization is presently handy and useful as a test case. Expecting one Mathlib to do what is needed ten or more years from now appears to me to be untenable.

[Chris Henson]

Ruben Van de Velde said:

But what's the point?

I interpreted this question as asking what is the purpose of changing Classical.em to an axiom when it seems this is not required for the dependency analysis.

[Riccardo Brasca]

Yes, I agree that different people have different goals and there is not such a thing as a perfect library.

Here I exactly want to see how complicated is to maintain a parallel version of mathlib that is adapted to what I am interested in at the moment. Since AFAIK it's a pretty new thing I think it is reasonable to start with very humble goals, and is especially important to keep the diff as small as possible. We all know how painful is to bump mathlib in a downstream project, and merging master after a lot of modifications, possibly to core, batteries and mathlib, can become very quickly a nightmare.

Let's see if this is doable in a specific case, then people are of course free to do the same with their favorite theory (for example I think that adding unique choice is a very reasonable thing to do, but again, this is not the point).

[François G. Dorais]

Ruben Van de Velde said:

But what's the point?

How else can you tweak core and have all of mathlib built for you automatically?

[Chris Henson]

This was the point of my suggestion towards the beginning of the thread about a command elab for reproving theorems. My idea is that we don't need to rebuild anything upstream, just provide an alternate proof that is shown to not make use of whatever Classical constants we would like to avoid. (Then this updates our notion of dependency)

[François G. Dorais]

If you don't have it already, you can request write access to Mathlib Testing so you can tweak the lean4-pr-testing branch too.

[François G. Dorais]

Chris Henson said:

This was the point of my suggestion towards the beginning of the thread about a command elab for reproving theorems. My idea is that we don't need to rebuild anything upstream, just provide an alternate proof that is shown to not make use of whatever Classical constants we would like to avoid. (Then this updates our notion of dependency)

That sounds like maximizing work for minimal effect. The saying is that Lean automation freely uses Classical.choice. In reality, almost none of this automation uses choice directly, they mostly use some degree of excluded middle. I would bet that changing Classical.em to an axiom instead of a theorem that uses Classical.choice will dramatically decrease the uses of choice everywhere.

[Chris Henson]

If you just need a one time analysis of the effect of this one change, I completely agree. It is worth doing to measure the effect of choice being used just for excluded middle.

What was asked about though was how to "maintain a parallel version [of Mathlib] that depends less on choice", which I seem to have interpreted differently. For this I think there can be an upfront cost (I think relatively modest) of some metaprogramming, but then in return you get the ability to have a repo downstream of Mathlib that achieves this goal while having a very ordinary process of further updates to Lean and Mathlib.

[James E Hanson]

François G. Dorais said:

Classical.em doesn't prevent Type u to be internally intuitionistic. It mostly means that you're using classical logic to reason about Type u. There are a few small consequences to this, such as Markov's Prinicple, ∀ (p : Nat → Bool), ¬(∀ n, p n) → (∃ n, p n), which is provable using Classical.em.

I would bet that Markov's principle is also not acceptable from the point of view of synthetic differential geometry.

[James E Hanson]

Also, if Prop is classical but Type u is internally intuitionistic, what type is the subobject classifier?

[Riccardo Brasca]

Chris Henson said:

If you just need a one time analysis of the effect of this one change, I completely agree. It is worth doing to measure the effect of choice being used just for excluded middle.

What was asked about though was how to "maintain a parallel version [of Mathlib] that depends less on choice", which I seem to have interpreted differently. For this I think there can be an upfront cost (I think relatively modest) of some metaprogramming, but then in return you get the ability to have a repo downstream of Mathlib that achieves this goal while having a very ordinary process of further updates to Lean and Mathlib.

Do I understand correctly that you are saying it is possible to override the current, say, List.nodup_range with a theorem with the same name but with a different proof and only acting on mathlib? This would be the perfect solution, but not that this is in a very basic file, so for example you need to be sure your metacode doesn't use the original, choice dependent, version.

[Riccardo Brasca]

Anyway I think the branch in nightly#188 does more or less what I want: it depends on the modified version of core and it has only a one line modification with respect to mathlb. I waiting for the cache, but it seems what I wanted.

[James E Hanson]

Riccardo Brasca said:

Do I understand correctly that you are saying it is possible to override the current, say, List.nodup_range with a theorem with the same name but with a different proof and only acting on mathlib?

What do you mean by only acting on mathlib?

[Riccardo Brasca]

not touching core, so without messing up with toolchains and stuff like that.

[James E Hanson]

What are you afraid it would mess up exactly?

[Chris Henson]

@Riccardo Brasca I am imagining a syntax like

reprove List.nodup_range := ...

where it looks up the existing declaration, requires a proof of the same signature not using choice, then registers this in a list of constants that have been reproven without choice.

[James E Hanson]

I'm asking because it's relatively easy to use environment hacking to just replace an existing definition/theorem with a different one (or even with an axiom). This would apply to the environment in which you prove theorems, but it wouldn't affect things like metaprogramming.

[James E Hanson]

One could in principle use this to check how many theorems in Mathlib really use choice rather than just LEM, for instance.

[Riccardo Brasca]

I am not afraid of messing up things, I am just wondering what is the easiest solution in practice. Something that allows me to update core/batteries/mathlib without suffering too much.

[Chris Henson]

Directly manipulating the environment is an interesting alternative, though I'm more paranoid about unintended consequences.

[François G. Dorais]

Riccardo Brasca said:

I am not afraid of messing up things, I am just wondering what is the easiest solution in practice. Something that allows me to update core/batteries/mathlib without suffering too much.

Like I said earlier, make a draft PR on Lean Core. Then you get CI to build Mathlib. It takes a while to build but it's way more convenient than a local build. You also get build cache... There's really no downside.

[Riccardo Brasca]

I already did that and I am testing everything. I am not familiar with the process so I am a little slow, but so far so good.

[Riccardo Brasca]

The core PR is lean4#12635 and with the corresponding branch lean-pr-testing-12635 on mathlib4-nightly-testing. Since I also want to modify mathlib I opened nightly#188 to see the diff. Testing on my project now.

[François G. Dorais]

James E Hanson said:

I would bet that Markov's principle is also not acceptable from the point of view of synthetic differential geometry.

I'm curious how that would matter, Markov's principle is generally used to prove that: "if it's not true that a Turing machine never terminates, then it terminates." That's a very mild assumption, often called "Russian School Constructivism".

[François G. Dorais]

Riccardo Brasca said:

The core PR is lean4#12635 and with the corresponding branch lean-pr-testing-12635 on mathlib4-nightly-testing. Since I also want to modify mathlib I opened nightly#188 to see the diff. Testing on my project now.

You should PR into Mathlib, not Mathlib Testing.

[Riccardo Brasca]

but then I see all the diff wrt to current mathlib, and this is completely unrelated to the modifications I made.

[François G. Dorais]

Can't you see the diff from your pr branch?

[François G. Dorais]

I'm asking because I never saw the need to do this so I'm curious what additional info you get?

[James E Hanson]

François G. Dorais said:

I'm curious how that would matter, Markov's principle is generally used to prove that: "if it's not true that a Turing machine never terminates, then it terminates." That's a very mild assumption, often called "Russian School Constructivism".

Markov's principle tends to not hold in toposes of sheaves, and my understanding is that the commonly considered models of SDG are closely related to toposes of sheaves (although I can't find anything about whether they satisfy MP in particular at the moment).

Beyond that, constructive mathematicians generally don't like to assume MP unless they have to, and more specifically the fact that it is provable in this context at all feels like a sign that maybe more is provable that you wouldn't want for SDG.

[Riccardo Brasca]

Here the diff wrt to master. Unless I misunderstood something it is huge.

[Riccardo Brasca]

mmm, it is huge because of set_option backward.isDefEq.respectTransparency false in. Maybe this is not the best week to try to play with modifications in core :sweat_smile:

[Robin Arnez]

Well if you want to test a Lean change against mathlib you'll need all the fixes for stuff between the latest release and your PR and these are on mathlib4-nightly-testing. And you conveniently get a branch there if you have a Lean PR with passing CI so it's quite natural to add onto that instead of mathlib directly.

[Riccardo Brasca]

Anyway, lean4#12635 is +18-7 and nightly#188 is a one liner modification. And the script gives... 1296 declarations don't depend on choice anymore.

[Riccardo Brasca]

Robin Arnez said:

Well if you want to test a Lean change against mathlib you'll need all the fixes for stuff between the latest release and your PR and these are on mathlib4-nightly-testing. And you conveniently get a branch there if you have a Lean PR with passing CI so it's quite natural to add onto that instead of mathlib directly.

Yeah, that is my point. All the rest is unrelated to what I am doing.

[Yury G. Kudryashov]

If you want it to land to Mathlib master, then you should add an attribute @[allowedAxioms] that checks if a declaration uses these axioms only, and reports one of the "top" level dependencies that causes unwanted dependency, if there are any.

[Yury G. Kudryashov]

(and tag theorems you care about with @[allowedAxioms .noChoice] or @[allowedAxioms -choice] - not sure which syntax is better)

[François G. Dorais]

Wow! It looks like you accidentally found a new way to mangle the setup. Not sure how that happened. Do you mind if I have a try at fixing it?

[Riccardo Brasca]

@François G. Dorais are you talking to me? Feel free to do whatever you want!

[Yury G. Kudryashov]

Then you'll have to convince the FRO to merge the core PR, of course. AFAIR, Leo didn't want to support classical reasoning with arguments along the lines of "not important enough to think about not breaking it".

[Robin Arnez]

What do you mean? How is this mangled?

[James E Hanson]

Yury G. Kudryashov said:

AFAIR, Leo didn't want to support classical reasoning with arguments along the lines of "not important enough to think about not breaking it".

Did you mean to say 'non-classical reasoning'?

[Riccardo Brasca]

Yury G. Kudryashov said:

Then you'll have to convince the FRO to merge the core PR, of course. AFAIR, Leo didn't want to support classical reasoning with arguments along the lines of "not important enough to think about not breaking it".

This is exactly why I am going through this process of having a modified version of core. I perfectly know it's almost impossible such a thing is going to be accepted, and even if it is it's just a matter of time before I will find another use of grind getting choice into the story.

I don't want to change the official version of core, not even mathlib. I just want to make it easy in practice to use my version, and available to anyone is interested.

[François G. Dorais]

@Yury G. Kudryashov That is not useful. The only way to change Leo's mind is to provide a product that meets in the middle, ideally with no compromises on Leo's part. This is _not_ impossible. The product is the key part.

[François G. Dorais]

Riccardo Brasca said:

François G. Dorais are you talking to me? Feel free to do whatever you want!

I just shuffled the mess, sorry :sad: Revert if you want. There were some recent changes that may be making things different from what I normally expect. I'll look at it again tomorrow...

[Riccardo Brasca]

No worries! I am force pushing the branch on my computer, without your last commits.

[Violeta Hernández]

I'd have no issue with an allowed_axioms tag used for whatever basic subset of Mathlib we want to keep choice out of. I'm fine with this, as long as the subset stays small. The moment that we have to start doing any sort of sacrifices in design is the moment where I feel like the cost outweighs the gains.

[Violeta Hernández]

An example I like to give. In the CGT repo, the basic type of games CGT#IGame requires choice to even define, for technical reasons that boil down to the usage of docs#Shrink. But the benefit is that we can get to proving stuff on games as they are defined in the literature almost immediately.

Meanwhile, Mathlib has a nearly analogous type docs#ZFSet (which is really just a one-sided game), which doesn't require choice, but it does require an auxiliary type docs#PSet with no mathematical meaning, as well as hundreds of lines of API where we define functions and relations on this type, so we can later lift them via a convoluted quotient. These are the sorts of situations where I feel like avoiding choice is just a hindrance.

[Niels Voss]

Do I understand correctly that your goal is to eventually (or figure out whether it is theoretically possible to eventually) reason about objects within Lean+3 axioms by defining an internal logic, proving theorems in Lean+2 axioms, and then using metaprogramming to transform proofs in Lean+2 axioms into proof objects in Lean+3 axioms?

If so, I wonder if the fact that certain theorems are proven without choice can be implemented at the time the metaprogram is run rather than requiring theorems to be proven directly in Lean+2 axioms. I'm not quite sure how to describe it, but I'm imagining a sort of predicate like ProvableWithoutChoice, where ProvableWithoutChoice P is to P as ComputablePred P is to DecidablePred P. That is, ultimately all we care about is the proof of ProvableWithoutChoice P and while one way to prove this is to prove P in Lean+2 axioms and then run a metaprogram on that proof, another way is to start with a proof of P in Lean+3 axioms and run a metaprogram on it to eliminate uses of Classical.choice (which could would by performing substitutions where if P depends on Classical.choice through referencing a proof of Q but there is also a proof of ProvableWithoutChoice Q, then the metaprogram could eliminate the reference to Q).

The design principle I'm imagining is that the result of #print axioms should not become part of the public API of a lemma. Instead, to record if a lemma's proof doesn't use choice, we could do something like

@[create_metaproof (allowed_axioms := [`propext, `Quot.sound])]
public theorem my_theorem : P := ...

which would, using the same mechanism as @[to_additive], generate an additional declaration, which is my_theorem.metaproof : ProvableWithoutChoice P. Importantly, the proof of my_theorem is not allowed to use the tactic classical but it is allowed to reference another theorem Q whose proof depends on Classical.choice, as long as a ProvableWithoutChoice Q exists somewhere.

I'm not arguing that this would actually be easier than simply sectioning off part of Mathlib to not use choice (and my proposal requires you to be choice-conscious in early parts of Mathlib anyways), but I think that if you want to use choice-free proofs to prove things about internal objects, you need some sort of meta-proof registry anyways (to avoid re-scanning all of mathlib over and over again) and you might as well build the choice-free proofs system into the meta-proof registry anyways rather than trying to make the result of #print axioms part of the public API of a lemma. It also allows you to record that things in core don't depend on choice without actually having to modify core.

[Aaron Liu]

Niels Voss said:

I'm not quite sure how to describe it, but I'm imagining a sort of predicate like ProvableWithoutChoice, where ProvableWithoutChoice P is to P as ComputablePred P is to DecidablePred P.

Note that to do this, ProvableWithoutChoice can't just be a predicate Prop → Prop in the same way that ComputablePred is just a predicate of type {α : Type u} → [Primcodable α] → (α → Prop) → Prop. Because Lean (with choice) proves there are in total only four predicates of type Prop → Prop! They are the constant functions fun _ => True, fun _ => False, as well as id and Not. So in order to be something sensible ProvableWithoutChoice has to be doing something weird to distinguish equal inputs.

[Niels Voss]

That's a good point; you would need some sort of parsing algorithm similar to Std.Do.SPred or a proof theory defined on Expr (like maybe something like lean4lean), which makes things much more complicated than I realized, and removes some of the benefits of my proposed approach.

[Riccardo Brasca]

A related dream (but this really just a dream) is to have a toposify or externalize tactic that takes a choice free proof about R-modules and proves the same theorem (in the appropriate sense) for sheaf of modules.

[Riccardo Brasca]

If someone wants to play with my branches note that I closed lean4#12635 and opened lean4#12637 that, if I didn't mess anything up, is based on 4.29-rc1, that is what current mathlib is using. The idea is then to have a branch of batteries using this the modified toolchain and then a PR to mathlib (not nightly testing) using the new toolchain and batteries. In this way this should be identical to current mathlib master except for the modifications I made, and it totally unrelated to nightly stuff.

[Edward van de Meent]

Aaron Liu said:

Niels Voss said:

I'm not quite sure how to describe it, but I'm imagining a sort of predicate like ProvableWithoutChoice, where ProvableWithoutChoice P is to P as ComputablePred P is to DecidablePred P.

Note that to do this, ProvableWithoutChoice can't just be a predicate Prop → Prop in the same way that ComputablePred is just a predicate of type {α : Type u} → [Primcodable α] → (α → Prop) → Prop. Because Lean (with choice) proves there are in total only four predicates of type Prop → Prop! They are the constant functions fun _ => True, fun _ => False, as well as id and Not. So in order to be something sensible ProvableWithoutChoice has to be doing something weird to distinguish equal inputs.

Indeed, the right way to do this is probably by having a type of proofs Proof, as well as a type class Proof.Proves and a predicate Proof.IsNonClassical?

[Trebor Huang]

François G. Dorais said:

I'm curious how that would matter, Markov's principle is generally used to prove that: "if it's not true that a Turing machine never terminates, then it terminates." That's a very mild assumption, often called "Russian School Constructivism".

It is only a mild assumption when your motivation for constructive logic is through computation. If you're coming from geometry, even when your metatheory is classical, Markov's principle holds when the topology is sufficiently regular. I don't have a good intuition for when it holds over gros sites, but one datapoint is that it holds for synthetic Stone duality.

[Riccardo Brasca]

Still not an expert, but in the internal logic of the small zariski site of a scheme X the structure sheaf becomes a non reduced field, or something like that, anyway an object that classically obviously does not exist. In synthetic differential geometry the situation is very similar, the main object is a ring with a property that classically is impossible.

[Kevin Buzzard]

If your ultimate goal is "turn this proof about modules into a proof about sheaves of modules" then my guess is that what you're suggesting (a huge foundational upheaval) is not the way to go about this. Usually the way to write a tactic is to come up with some easy examples of what you want it to do, and then write code which does then, and then try and figure out how to write meta code which produces this code. Do you have any concrete toy examples of theorems about sheaves of modules that you want to prove using this method? I'm wondering if this choice-removal is a red herring.

[Riccardo Brasca]

My current concrete goal is to see if it is possible to formalize in Lean and using mahtlib, the internal logic of synthetic differential geometry. This is an intuitionistic theory so I cannot use mathlib's theorem that depend on choice, and this is why I am reproving them without choice. I perfectly realize that not a lot people will care about this goal, and that probably other proof assistants are better in avoiding choice. I am just curious to see in practice how difficult is to do the same with mathlib. (And honestly I am already happy I've learnt how to build a toolchain.)

The rest is just publicity to advertise this kind of problems, but I don't expect to have anything concrete soon (unless someone else gets involved). Anyway, experts tell me that, as an example where this approach of working internally in a topos really helps, is to show that a sheaf of $\mathcal{O}_X$-modules on a reduced scheme $X$ is locally free on a dense subset of $X$. But again, I don't think setting up all the machinery is easier than just proving the lemma (and I don't even know if it possibile to set up the machinery).

[Riccardo Brasca]

Anyway, to people who want to experiment:

• lean4#12637 is the PR to core, that creates the toolchain lean4-pr-releases:pr-release-12637, where a couples of basic results about lists don't depend on choice anymore.
• batteries#1690 uses the batteries branch riccardo/less_choice that in turn uses the toolchain above. Currently this is the only modification, but it seems likely something will have to be changed even in batteries.
• #35641 is a "normal" mathlib PR, but uses the toolchain and batteries mentioned above. Note that it is a PR to master, so the diff you see is the real one, in practice it can be treated as any other PR (but I don't want to merge it, I just want the cache!).

As you can see the diff is very small, but already with so few modifications to mathlib (+ dependencies) we go from 387284 declarations using choice to 385303. I understand it's not super interesting for mathematicians, but technically this means 1981 theorems now have one less assumption.

[Kevin Buzzard]

I'm aware of this claim about a sheaf being locally free on a dense subset being an application of constructive methods in algebraic geometry; what I'm saying is that if your actual goal is this then I think the first step isn't the foundational upheaval, the first step is writing a proof of the module statement (the not not free thing) without using choice, and then writing a proof of the sheaf statement in the form which you ultimately want the tactic to produce. Then you can take stock and ask whether you actually need the foundational upheaval in order to get there, or whether you can simply make the tactic without the foundational upheaval, instead being "inspired by the foundational upheaval".

[Kevin Buzzard]

I think what I'm saying is that if your goal is to remove AC from the proofs of certain specific statements, then you might want to try writing down those proofs first and seeing where AC is used, rather than trying to remove AC from the proofs of as many statements as possible via some kind of splattergun approach, and hoping you get lucky.

[Riccardo Brasca]

This is what I am doing now (I started a couple of days ago, so I don't know where it is going). For example one can see that Finset.image depends on choice. Why? It's not easy to guess, but in this case it turned out quite easy to remove the dependency by hand, and I am happy about it (since in my project I want to manipulate various sums I need Finset.image). Something should be doable with a bit of metaprogramming (and I want to learn how to do it!) is to find, given a declaration X, the list of declarations Y used in the proof of X that depend on choice in a minimal sense (those directly connected to choice in the graph of dependencies, if X uses A that uses B that uses C that uses choice I want to see C, not A and B).

[Riccardo Brasca]

So maybe my personal motivation is just to learn something new rather than proving another theorem, but if people find the approach interesting even better!

[Kevin Buzzard]

Come to London, we have metaprogramming experts here :-)

[Kevin Buzzard]

Here is a question about the topos application to alg geometry: if you take the statement about modules, and write the proof in full, then presumably the corresponding statement and proof about sheaves of modules is literally some kind of line by line translation, so in some sense it's the same as what to_additive is doing? I think it would be very instructive to write both proofs in full so that one can see exactly what the translation process looks like in practice.

[Riccardo Brasca]

Kevin Buzzard said:

Come to London, we have metaprogramming experts here :-)

I am arriving in March!

[Edward van de Meent]

Kevin Buzzard said:

Here is a question about the topos application to alg geometry: if you take the statement about modules, and write the proof in full, then presumably the corresponding statement and proof about sheaves of modules is literally some kind of line by line translation, so in some sense it's the same as what to_additive is doing? I think it would be very instructive to write both proofs in full so that one can see exactly what the translation process looks like in practice.

i think this is good for getting intuition, but if we want something of this shape in mathlib, we should wait untill we have the internal language of topoi formalized in mathlib, since what you're suggesting includes proofs of "this notion on sheaves corresponds to this internal notion" as well as "the ususal rules of deduction are sound in the internal language of a topos".

[Edward van de Meent]

and only the second part of that is relevant to any potential metaprogram, i think

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Edward van de Meent said:

Indeed, the right way to do this is probably by having a type of proofs Proof, as well as a type class Proof.Proves and a predicate Proof.IsNonClassical?

We have been working on this machinery in HoTTLean. (We are interested in models of HoTT there, but the machinery is general and also applicable to sheaf models of SDG).

We are working in type theory so there isn't exactly a type of Proofs but rather a type of terms-of-some-type; but that's probably what you meant anyway. Our analogue of the create_metaproof attribute that @Niels Voss suggested is @[reflect]. It takes a Lean definition and produces a deeply embedded "reflection", i.e., given def foo : T := a, it produces a (Lean) proof that 𝕋 ∣ · ⊢ a : T which we can read as "type theory proves that a is a closed term of type T using axioms 𝕋". Then ProvableWithoutChoice/Proof.IsNonClassical amounts to Classical.choice ∉ 𝕋. See here for some example uses. (Btw, @[reflect] has already been discussed back in 2021).

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kevin Buzzard said:

Do you have any concrete toy examples of theorems about sheaves of modules that you want to prove using this method?

One example that Ingo Blechschmidt sometimes highlights is as follows. (I am no algebraic geometer, so apologies for any potential mistakes.) Let $𝒪_X$ be the structure sheaf of a ringed space, and let $0 → M_1 → M_2 → M_3 → 0$ be an exact sequence of sheaves of modules over $𝒪_X$. If $M_1$ and $M_3$ are of finite type, then so is $M_2$. (Is this in mathlib? I couldn't find it by Stacks tag 01B7.) Then the way to prove this via toposify is to translate a constructive proof of the "de-sheafified" statement which is as follows. Let $0 → M_1 → M_2 → M_3 → 0$ be an exact sequence of modules. If the outer ones are finitely generated, then the middle one is as well. (docs#Module.Finite.of_exact).

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kevin Buzzard said:

if you take the statement about modules, and write the proof in full, then presumably the corresponding statement and proof about sheaves of modules is literally some kind of line by line translation

It's not super clear to me what line-by-line might mean for Lean proof terms. Let me interpret that as "a metaprogram that takes a Lean.Expr of the internal proof (e.g. in constructive ring theory) and produces another Lean.Expr for the external one (e.g. about sheaves) by a somewhat direct recursion". There is a sort of syntactic, recursive translation from constructive-internal-statement to sheaf-statement given by Kripke-Joyal semantics, but this is for translating statements, not proofs. I have once attempted to translate proof terms concurrently with K-J, so perhaps the sort of thing you mean. I ran into so many issues that I am now convinced the correct approach is rather what we are doing with HoTTLean, deep embedding of type theory and all. But I don't mean to discourage anyone from trying!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Edward van de Meent said:

if we want something of this shape in mathlib, we should wait untill we have the internal language of topoi formalized in mathlib, since what you're suggesting includes proofs of "this notion on sheaves corresponds to this internal notion" as well as "the ususal rules of deduction are sound in the internal language of a topos"

I should remark on one thing: it is common to talk about the 'internal language of topoi', but in classical literature that language is some kind of higher-order logic rather than dependent type theory (so more like Isabelle than Lean). Actually interpreting dependent type theory in a (let's say sheaf) topos remains an active area of research. One obstacle is that it's technically challenging to build a universe in such a topos (see e.g. Strict universes for Grothendieck topoi for one construction), and you need a universe if the internal logic is to support a Type universe. One would probably struggle to do any math in Lean without quantifying over Type! So what we have in HoTTLean is a 'natural model' which one could think of as an adjusted definition of topos that assumes you have already solved this problem. (See also this previous discussion.)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

FInally, with apologies for hijacking this thread somewhat, I also have a call to action for those interested in developing the hypothetical toposify. I believe the HoTTLean approach is promising, but there are many technical problems to solve before it can be used for anything like those sheaf-of-modules statements or SDG. To list some, we only support a very minimal fragment of Lean, there are performance issues in the @[reflect] macro, and we don't quite know how to effectively work with "this notion on sheaves corresponds to this internal notion" yet. (I also discussed some of these in my talk on Thursday.) I think there are paths to solving these, but it will require effort. We are actively looking for help and new contributors! If there is enough interest, maybe we could even start a Zulip stream for the project?

[François G. Dorais]

I agree. This issue needs a team with both theory experts (in topos theory and type theory) and expert users (for API and applications). I would be happy to engage in such a team.

[Riccardo Brasca]

Going back the experiment I described at the beginning, the main place for having a look is now #35685.

[Riccardo Brasca]

By the way, I am writing an article on synthetic differential geometry with @Gabriella Clemente, you can see the code here.