constructive tactic mode in lean

Stream: lean4

[Bulhwi Cha]

Mario Carneiro said:

Joe Hendrix said:

Are there problems with that PR that I should be aware of?

I see that you made simp much more aggressively classical than before, making use of Classical.foo lemmas even when Decidable.foo lemmas could be used to similar effect (such that classical simping can be controlled by open Classical). This makes me sad, I was trying to avoid that, but I'm not really able to keep arguing on this point.

(what's worse, making them global simps in core means no one can override it in downstream projects without local un-simp-ing every time)

Are we not going to be able to use tactic mode constructively in Lean? Wouldn't it be better if Lean allowed each user to choose whether to use classical logic in tactic mode?

[Bulhwi Cha]

I think Lean could've been more inclusive.

[Mario Carneiro]

see also lean4#2414

[Eric Wieser]

(and the very simple patch at lean4#2412 that was deemed too much of a maintenance burden)

[Bulhwi Cha]

Scott Morrison said:

We're not at a point presently where changes like this are likely to be accepted in core. I appreciate this is unfortunate for people doing constructive maths, but in the medium term it's not a priority, and will have to be supported by separate libraries that redo foundations lemmas and tactics as required.

Currently, Lean isn't designed to support constructive theories. Therefore, the following explanation in Chapter Axioms and Computation of #tpil is false:

Lean is designed to support both of these approaches. Core parts of the library are developed constructively, but the system also provides support for carrying out classical mathematical reasoning.

[Bulhwi Cha]

Can I make a pull request that fixes the misleading passage above?

[Bulhwi Cha]

Leonardo de Moura said:

We are always listening to our users. We have talked to many mathematicians and computer scientists, and the vast majority don't care about constructivism. I have asked about high impact projects that are currently blocked unnecessary uses of Classical.em, and never got a convincing answer :smile:

We won't get an answer because few constructivists will use Lean. Why would they do so when the core developers keep making it hard to use tactic mode constructively in Lean?

[Bulhwi Cha]

If we follow Leo's logic in the above quote, I can create the following scenario:

In 2077, Bulhwi launched the Bean project, his fork of Lean. Since almost every Bean user is Korean, he wrote all documentation for Bean exclusively in Korean. One day, Vee, an English speaker, asked Bulhwi to translate Bean's documentation into English, but he declined. Bulhwi said, "Vee, I've talked to many Bean users, and the vast majority don't care about English translation. I've asked about high-impact projects whose developers are struggling due to lack of English documentation, and I've never got a convincing answer."

[Julian Berman]

Without a horse in the game, that seems like a bit of a straw man to me. From a pure maintenance standpoint that closed PR makes some bit of sense to me personally. There's always someone saying "OK you don't want to work to support X, but if you just do this little piece then I can do X myself", and it seems like the response is simply "we aren't ready to support X in any form, and don't want to merge things that make it even seem like we are". I think often the "metareason" is "you say it's just this little thing, but then 3 others pop up, and we don't care". The overall message I'd take personally seemed like "try again later", which is annoying but not a firm no? In the straw man though, it would certainly be wrong to conclude "no one cares about X" from the current state of the world. Though certainly the hypothetical future where people who do care about X don't use Lean seems likely if Lean doesn't have X.

[Bulhwi Cha]

Julian Berman said:

From a pure maintenance standpoint that closed PR makes some bit of sense to me personally. … The overall message I'd take personally seemed like "try again later", which is annoying but not a firm no?

I agree with you to some extent, but I also want to point out that the Lean core developers still haven't fixed the misleading explanation in their standard reference:

Lean is designed to support both of these approaches. Core parts of the library are developed constructively, but the system also provides support for carrying out classical mathematical reasoning.

They should clarify that Lean will support classical logic exclusively.

[Bulhwi Cha]

I'll make a PR after I wake up. By the way, I learned Lean 4 by reading the text thoroughly two years ago.

[Henrik Böving]

They should clarify that Lean will support classical logic exclusively.

But that is not true, you can very much write your proofs without classical logic and you can develop automation to do things without classical logic, the foundational system is not stopping you from doing this. It just that the core provided tactics might use classical logic under the hood, even if there are scenarios where they might not have to. You can write tactics that will not use classic logic at all if you choose to do that. But if you have a use case for that beyond "it is possible so let's do it" I'm sure the core team would be happen to listen to you and re-evaluate the current stance. As Leo explains in his quote the issue is that he has not been presented with such a use case yet.

[Kim Morrison]

Eric Wieser said:

(and the very simple patch at lean4#2412 that was deemed too much of a maintenance burden)

I think this is a bit misleading. It's not that patch itself that would be a maintenance burden. There problem is that classical reasoning runs deep in some places, and we are not interested in getting in a situation where there are more and more PRs to review asking for changes in the tactic framework to support constructivism (without compelling evidence that this would enable significant new applications of Lean --- something we remain pretty sceptical of at present).

There's evidence I think that this stuff is prone to consuming oxygen -- I've seen multiple conversations in which there's been an argument about whether classical reasoning in termination proofs matters (it doesn't!), and certainly there's also the burnout effect where Lean 2 invested significant effort to support HoTT, only to realise it was not relevant to Lean's goals, and we really don't want a repeat of that with constructivism.

I don't keep track of this, but perhaps someone could confirm my memory that even the equation compiler is implicated in "unnecessarily classical"? We really really don't want to consume cycles talking about changes for that.

[Thomas Murrills]

I don't personally care about constructivism, but my soft case for supporting constructive proofs out of the box is more or less "there are some really interesting people doing things constructively, and if they were able to work (easily) in Lean, then the Lean community, the Lean ecosystem, and, indirectly, Lean itself would be better for their presence."

Now, I'm not saying that from this alone we should necessarily conclude that supporting constructivism is worth it, as there are (as mentioned) significant costs to weigh. But perhaps it's a factor to consider alongside the others. There's something to be said for being usable by everyone.

[Kim Morrison]

Regarding tpil, we're in a quiet period at the moment for maintenance of tpil, but when that resumes I think it would be reasonable to clarify that while Lean's type theory is not classical, the tactic framework provided with the core language freely uses classical reasoning, and that any serious constructive project would either need to be very careful about what tactics it used, or build alternatives externally.

[Eric Wieser]

TPIL isn't (currently) owned by the FRO, right? (not that I'm saying it would be a problem if it were)

[Kim Morrison]

Thomas Murrills said:

"there are some really interesting people doing things constructively"

To be honest I hear this, but don't see it. The interesting things keep appearing to me as fun curiosities, but that don't actually lead anywhere. I know it's unreasonable to ask for Lean examples, but perhaps someone could point to major projects in Coq/Isabelle/etc that really rely on constructivity and that we should be sad we are missing out on?

If @Kevin Buzzard were to announce when he reveals his roadmap for FLT that he really needs support for constructivism for parts of the project, we would absolutely be on it tomorrow.

Now I appreciate that is a straw-man argument --- Kevin is not about to say this! So can someone help me come up with the steel-man alternative?

[Kim Morrison]

Eric Wieser said:

TPIL isn't (currently) owned by the FRO, right? (not that I'm saying it would be a problem if it were)

My understanding is that the most likely person to put significant work into it is perhaps @David Thrane Christiansen (but not immediately!). Jeremy has done a lot of work on it, but doesn't have much time for it at present.

[Eric Wieser]

Yes, it's very clear to me that Verso is intended to provide new foundations for TPIL when it is sufficiently mature.

[Eric Wieser]

Scott Morrison said:

The interesting things keep appearing to me as fun curiosities, but that don't actually lead anywhere.

I suspect the interestingness is rather subjective, and most of the people currently using Lean are the ones who already decided that these questions don't interest them at all. Of course, the same reasoning applies to HoTT; but I think the burden of HoTT support is much greater than that of (partial) constructivity support.

[Eric Wieser]

In my mind, the main argument in favor of lean4#2412 is that if you are a constructive user who has decided to rebuild the Lean universe constructively, this small change greatly increases the fraction of the universe that doesn't need to be discarded. My very limited understanding of HoTT is that things are fundamentally much more different than just avoiding an axiom.

[Eric Wieser]

(it also has the nice bonus that it could result in split and split_ifs being merged)

[Eric Wieser]

Of course, the counter-argument is that users who want to rebuild the universe are trouble :)

[Thomas Murrills]

Scott Morrison said:

"there are some really interesting people doing things constructively"

To be honest I hear this, but don't see it. The interesting things keep appearing to me as fun curiosities, but that don't actually lead anywhere

Sure—my point is not that people are doing interesting things, but that there are interesting people doing these things. And I believe they would contribute positively to Lean if they had a place in the community.

[Thomas Murrills]

With the understanding, of course, that "contributing positively" is not measured only by use cases. If someone gets people talking about Lean, if they introduce it to students or friends, if they explore something unusual, if they find a bug, if they simply participate in conversations, then regardless of what you think about the projects this person is spending their time on—even if they never contribute something you care about—they're building a stronger community around Lean simply by using it, showing it to others, and being involved.

[Thomas Murrills]

(As an aside, I'd be reluctant to discount some math selectively as fun curiosities that don't actually lead anywhere—I mean, we are doing math, after all, which is famous for garnering that opinion, no matter what field you work in! :wink: Separately, I think that in general there's intrinsic value to supporting someone's ability to do something they value, in and of itself, of course—but I want to emphasize that this not a factor in my point above. There, I'm trying to take a "self-centered" view "from Lean's perspective".)

[Henrik Böving]

but that there are interesting people doing these things

Which people? I would really like to know, I've not seen a concrete project or name being brought up in these discussions yet.

[Thomas Murrills]

I mean, the people who are told to use Agda or Coq precisely because it's constructive—or perhaps the person who started this thread? :wink: For my anecdotal part, I attended the HoTT summer school a little while back, and met (and heard of) all sorts of people who at least were interested in constructivism. Type theorists, mainly? I forget the names, since I personally am not interested in constructivism. :grimacing: There's probably a sample bias here, because if you use Lean, you're likely already committed to classicality, so there likely aren't too many people who can answer that question—and this population is a minority in the first place.

But also, I saw people who were relatively early in their mathematical career who were interested in constructivism. Not that you're suggesting this, of course, but it's worth remembering that you don't need to be a "big name" to "be interesting" and contribute positively! :) I'm thinking about this in terms of building a community and attracting people in general, not in terms of attracting specific names.

And I will repeat just for emphasis that while I think this should be a factor, there are of course very good reasons for it not to be decisive once you look at the costs. :)

[Mario Carneiro]

Scott Morrison said:

I don't keep track of this, but perhaps someone could confirm my memory that even the equation compiler is implicated in "unnecessarily classical"? We really really don't want to consume cycles talking about changes for that.

Not to my knowledge, the core mechanisms used by both structural and WF recursion are choice-free. Termination proofs can still end up using choice if the WF proofs themselves, as generated by decreasing_by, use choice, but for the most part the automatic proof mechanisms are reasoning over functions on Nat and everything in sight is decidable there. (I would not be surprised if omega currently has some incidental uses of choice, but they should be easily removable without affecting the interface or effectiveness or even proof size in any way.)

[Patrick Massot]

I think that now is a really bad time to talk about constructivism in Lean. We already have a lot of work to do to figure out a good way to fully support both math and software verification. I think that adding a third incompatible set of users would be a huge waste of time and energy in the current situation. Maybe one day this will be possible.

[Kevin Buzzard]

It seems to be that this discussion is the idealists ("why not support more people who can use the software in new ways?") vs the realists ("there is a huge amount of work which needs to be done in order to attain the goals which the FRO has set so let's focus on that"). I also suspect that you become more of a realist as you get older and realise that time is less infinite than it used to be when you were a PhD student or post-doc.

[Bulhwi Cha]

Henrik Böving said:

Bulhwi Cha said:

They should clarify that Lean will support classical logic exclusively.

But that is not true, you can very much write your proofs without classical logic and you can develop automation to do things without classical logic, the foundational system is not stopping you from doing this. It just that the core provided tactics might use classical logic under the hood, even if there are scenarios where they might not have to. You can write tactics that will not use classic logic at all if you choose to do that.

I'll rephrase my statement: Lean core developers won't provide constructive tactic mode themselves. #tpil has never mentioned this. You can't expect newcomers to Lean to figure it out quickly. I hadn't until late 2023.

[Kevin Buzzard]

Maybe make a PR to #tpil ?

[Bulhwi Cha]

I'll do it after I have breakfast.

[Mario Carneiro]

I don't think "constructive tactic mode" should be a goal. But it is possible to build "constructive tactics" outside the core and ideally these could be used alongside the many tactics from core which also happen to be constructive

[Bulhwi Cha]

Henrik Böving said:

But if you have a use case for that beyond "it is possible so let's do it" I'm sure the core team would be happen to listen to you and re-evaluate the current stance. As Leo explains in his quote the issue is that he has not been presented with such a use case yet.

The core team made constructivists and type theorists don't want to use Lean in the first place. That's why they wouldn't and won't be able to find such a use case. It's far from "listening to others." But I'd say it's fine if the Lean developers had clearly stated on their documentation that they wouldn't develop constructive tactics themselves. They haven't.

Analogy

Bulhwi Cha said:

If we follow Leo's logic in the above quote, I can create the following scenario:

In 2077, Bulhwi launched the Bean project, his fork of Lean. Since almost every Bean user is Korean, he wrote all documentation for Bean exclusively in Korean. One day, Vee, an English speaker, asked Bulhwi to translate Bean's documentation into English, but he declined. Bulhwi said, "Vee, I've talked to many Bean users, and the vast majority don't care about English translation. I've asked about high-impact projects whose developers are struggling due to lack of English documentation, and I've never got a convincing answer."

@Henrik Böving Do you think the following statement isn't true? "The Bean project supports documentation exclusively in Korean."

You (Vee) can very much teach yourself Korean and translate the documentation into English without the maintainer's help; he isn't stopping you from doing this. It's just that the documentation he provided is written only in Korean, even if there are scenarios where a few English-speaking Bean users couldn't read it. But if you have a use case for that beyond "it's possible, so let's do it," I'm sure the maintainer would listen to you and re-evaluate the current (2077) stance. As Bean's maintainer explained in the above quote, the issue is that he's not been presented with such a use case yet.

[Jireh Loreaux]

I totally get not having infinite time and not wanting to devote extra hours to figuring out potentially complicated workarounds to make things constructive. But on the topic of lean4#2412 (which is incredibly simple), I think there has been more time spent arguing over It than there ever would have been in terms of maintenance burden.

Sometimes the easiest way to get a user base off your back is to appease them when it's easy. Of course, I don't subscribe to the idea that merging it requires core devs to take seriously any other change to support constructivism. There is no slippery slope.

[Bulhwi Cha]

Kevin Buzzard said:

Maybe make a PR to #tpil ?

I'm working on it.

[Bulhwi Cha]

From https://github.com/leanprover/theorem_proving_in_lean4/pull/110:

M introduction.md => introduction.md

 This tutorial describes the current version of Lean, known as Lean 4.

+You may want to reconsider your decision to learn Lean if you plan to use it for
+projects based on constructive logic. See [Section Historical and Philosophical
+Context](./axioms_and_computation.md#historical-and-philosophical-context).

 About this Book

M axioms_and_computation.md => axioms_and_computation.md

-Lean is designed to support both of these
-approaches. Core parts of the library are developed constructively,
-but the system also provides support for carrying out classical
-mathematical reasoning.
+
+Be aware that some tactics in Lean's core library use classical
+reasoning by default, even if a user has not opened the `Classical`
+namespace or used lemmas within it. Technically, it is still possible to
+build alternative tactics for constructive logic outside the core
+library and use them alongside the constructive tactics from the core.
+However, the developers of Lean's core library currently do not want to
+implement these tactics themselves, nor do they accept any changes that
+attempt to modify the tactics in the core to avoid using classical
+reasoning, regardless of how simple the change may be.

I've created a PR, and I'll apply this change to my fork of #tpil.

[Kim Morrison]

Seems unlikely to be a productive approach, but :woman_shrugging:.

[Bulhwi Cha]

I need a fork for some other reasons unrelated to this debate, anyway.

[Jireh Loreaux]

Bulhwi Cha that seems unnecessarily antagonistic.

[Bulhwi Cha]

Drew Devault said:

As a contributor, you should evaluate the value system of the leadership and make a personal determination as to whether or not it aligns with your own. If it does, participate. If it does not, find an alternative or fork the project.

Forcing a project leader to make a decision they don't want is unnecessarily antagonistic. Forking the project isn't. Rather, it's a reasonable resolution of a disagreement. The copyright holders of open-source software permit users to modify and distribute the software and its source code to anyone. Furthermore, I didn't make any false claims in the paragraphs I added to my fork.

[Bulhwi Cha]

You're welcome to suggest any improvements to my PR and fork. I promise to clarify that the changes I made to the original text aren't endorsed by the original authors of #tpil.

[David Thrane Christiansen]

Scott Morrison said:

Eric Wieser said:

TPIL isn't (currently) owned by the FRO, right? (not that I'm saying it would be a problem if it were)

My understanding is that the most likely person to put significant work into it is perhaps David Thrane Christiansen (but not immediately!). Jeremy has done a lot of work on it, but doesn't have much time for it at present.

The work that I'm putting into it right now is quite limited, and mostly consists of merging PRs that fix very simple things, like typos, and making the code examples work in newer Lean 4 releases. I don't presently have plans to embark on any major revisions, or to make substantial changes to the text. I may also port the contents to Verso once it's mature for this use case once we get real benefits from the port (e.g. more reliable cross-linking of documents, or better dogfood-style testing of the tool).

[Bulhwi Cha]

Jireh Loreaux said:

Bulhwi Cha that seems unnecessarily antagonistic.

Can you elaborate on this? Why do you think forking an open-source project is unnecessarily antagonistic?

[Siddhartha Gadgil]

I believe the reaction is to the words: "nor do they accept any changes that attempt to modify the tactics in the core to avoid using classical reasoning, regardless of how simple the change may be."

[Siddhartha Gadgil]

(deleted)

[Bulhwi Cha]

I understand that the part in bold sounds highly critical of the Lean core team, but they did close an "incredibly simple" pull request, which is lean4#2412. Eric Wieser and Jireh Loreaux have already pointed this out. It's clear that the Lean core team won't accept those kinds of changes larger than lean4#2412. Therefore, the wording in that part of the quote is pretty accurate. I didn't exaggerate.

Eric Wieser said:

(and the very simple patch at lean4#2412 that was deemed too much of a maintenance burden)

Jireh Loreaux said:

But on the topic of lean4#2412 (which is incredibly simple), I think there has been more time spent arguing over It than there ever would have been in terms of maintenance burden.

[Kyle Miller]

@Bulhwi Cha I'm a bit confused — are you personally interested in constructive mathematics? This is the first thread I've ever noticed you mention it. Is it the case that you've spent all this time learning Lean this far just because you were misled by a sentence in TPIL?

Regarding forks, while it's not illegal to make a fork, from a social perspective it's a last course of action, signaling that working together is impossible, and it's better to make a separate project. That's unless your 'fork' is actually just a copy where you'll do development that you intend to contribute (like Github's use of 'fork'), rather than a separate project that you intend to advertise and have compete with the original.

[Kyle Miller]

Regarding your Korean/English analogy, I see that as being a very different situation. People who do constructive mathematics can read and understand classical mathematics, and vice versa. In ITP communities, constructivists are very well represented, and compared to the number of constructivists in both computer science and mathematics, they are overrepresented, which is to say, despite what you hear, it's a relatively niche requirement. Lean not putting engineering effort into supporting constructivism is not stopping anyone from developing its "killer app", when there's Coq and Agda.

[Bulhwi Cha]

Kyle Miller said:

Bulhwi Cha I'm a bit confused — are you personally interested in constructive mathematics?

I'll answer this question before I go to sleep. Does it matter? I don't think so. You're missing the point.

[Kyle Miller]

I think it's generally good to spend energy on what you care about, vs only out of principle, or if it's out of principle, then it should be a principle that's well-motivated and one that you care about.

If you think TPIL is intentionally misleading you somehow, know it's an old document that goes back to the old days of Lean, and Lean has changed. And, overall, recently there hasn't been much energy put into updating documentation, vs put into improving Lean.

[Kyle Miller]

@Thomas Murrills I saw you mention the idea "supporting a feature will draw people", but from a product management perspective that's an easy way toward creating a product that supports every feature, but none well. I could say, for example, "if Lean supported object-oriented programming paradigms better, then it would draw all those people who are doing good work," and so on for every feature and paradigm.

For something like constructive math, Lean core wants a concrete story: having such-and-such feature enables such-and-such application.

I'd be reluctant to discount some math selectively as fun curiosities that don't actually lead anywhere

I think it's worth considering that while math and logic are closely aligned, mathematics as a whole is not particularly interested in foundational issues. The only place I've heard of where mathematics begins touching upon constructivism is internal logics of elementary toposes — my understanding is that making it possible to write constructive arguments means that you can transport statements and proofs into this internal logic. If somehow it's discovered that this is the best way to prove things about programs, for example, then that's a concrete story. (To be clear: I'm not discounting the work people do on foundations. It's just that for a project like Lean, which wants to be used wherever mathematics is traditionally used, I think at some point you have to commit to your foundations.)

[Kyle Miller]

One application of constructive mathematics that seems sort of compelling to me is that a proof written constructively could be reduced, giving a concrete reason that the theorem is true for some particular concrete inputs. However, it's known that with Lean's type theory, proof reduction doesn't always terminate: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Normalization.20fails.20in.20lean/near/409110365

[Mario Carneiro]

Kyle Miller said:

@Thomas Murrills I saw you mention the idea "supporting a feature will draw people", but from a product management perspective that's an easy way toward creating a product that supports every feature, but none well. I could say, for example, "if Lean supported object-oriented programming paradigms better, then it would draw all those people who are doing good work," and so on for every feature and paradigm.

Actually, I think "creating a product that supports every feature, but none well" is a fantastic choice for lean core, because it is extensible along almost every axis. Lean is the language that lets you build it in the direction you want, and this means it is applicable even to things that go far beyond the goal of proving theorems in Lean's particular choice of type theory and axioms. The way you leverage an extensible system is by not putting blockers to extending it in specific directions, because every user has a slightly different goal and may want to extend it in ways the original authors never dreamed of. This is okay, in fact it's what we should all be excited to see. It's one of the things I love about this community, watching all the cool and crazy things people are able to get lean to do.

I think the mistake here is taking all of the responsibility for building the feature itself into the core (which is the opposite of extensibility), because the people who want the feature are not the core maintainers themselves, it is the downstream users who are coming up with these ideas. Core wants to support the mean because that's where most people are. So cool and crazy extensions are necessarily not going to be getting direct support from core. But it should be "possible in principle", or even better "relatively straightforward", to build these things. The syntax system is a great example of this, we have people writing C code directly in lean or controlled natural languages and this is very different from what lean out of the box is designed to do, and yet it's not really a misuse either because this is what extensibility is for.

[Mario Carneiro]

Incidentally, regarding object oriented paradigms I think lean actually has most of the building blocks already: method syntax, structural inheritance, Dynamic types, imperative control flow. I 100% believe someone could build a passable java-ish syntax and/or semantics as a lean library.

[Mario Carneiro]

Kyle Miller said:

Regarding your Korean/English analogy, I see that as being a very different situation. People who do constructive mathematics can read and understand classical mathematics, and vice versa. In ITP communities, constructivists are very well represented, and compared to the number of constructivists in both computer science and mathematics, they are overrepresented, which is to say, despite what you hear, it's a relatively niche requirement. Lean not putting engineering effort into supporting constructivism is not stopping anyone from developing its "killer app", when there's Coq and Agda.

What this fails to consider is that maybe people might want to use lean for all its other features, when they are doing constructive math in Coq or Adga or what have you. Many of lean's unique innovations are in the realm of ITP structure generally, having this super-hackable whitebox everything approach to elaboration. In fact Lean's kernel / type theory is one of its least innovative aspects, mostly by design. For such people the path of least resistance may indeed be to either fork lean and rewrite the tactics, or possibly create a library that duplicates or copy pastes half of Lean in order to make the necessary patches (but is otherwise still built on a standard lean installation). I've certainly seen things like that done for academic projects in the past. The maintenance requirement of such a setup is high, but most academic projects don't get maintenance anyway, and the actual work might be much lower than getting all the fancy features of lean into Coq or Agda.

[Kevin Buzzard]

Mario suggests that core can support all of the people all of the time, but I don't think that's true. Aren't there constructivists out there who think that Lean's type theory itself is completely broken because of subject reduction or something? To support all of the people all of the time you'd have to have a system where you'd allow univalence, allow different Props, allow cubical etc etc. You have to draw the line somewhere.

[Mario Carneiro]

Actually my suggestion is not limited to those theories that extend lean's base type theory, because you can use Lean as a tactic language for deep embeddings too. Some examples of this include iris-lean, which formalizes an extensible intuitionistic higher order separation logic called Iris (originating from a Coq library of the same name and popular for formalizing programming language semantics), and lean4lean, which includes some metaprogramming for constructing derivations in the embedded lean logic (which is more of a pre-logic and does not assume all parts of lean's axiomatization at all times)

[Mario Carneiro]

I keep looking for HoTT enthusiasts willing to do HoTT metatheory in mathlib because I think this is the true way forward for HoTT in lean, not changing the base axioms

[Mario Carneiro]

I really want to see a crazy proof that the fundamental group of the circle (the actual circle not the synthetic HoTT one) is $\Bbb{Z}$ using embedding in a HoTT model

[Mario Carneiro]

core can support all of the people all of the time

That's not what I'm saying, or at least it depends on what you mean by "support" but not the usual reading of this. Core can get out of the way of most of the people almost all of the time. I don't want "support" I want non-interference

[Patrick Massot]

Then don’t use the tactics you don’t like!

[Bulhwi Cha]

They won't.

[Bulhwi Cha]

Kyle Miller said:

Is it the case that you've spent all this time learning Lean this far just because you were misled by a sentence in TPIL?

No. I think your wording here is inappropriate.

I learned Lean because I want to use it to develop an educational video game that teaches various topics in STEM disciplines. But I always struggle to describe the exact range of topics that my game will cover. I plan to include several kinds of non-classical logic in the game.

Proof assistants other than Lean might also be used in this game.

Quotes

Bulhwi Cha said:

I hope to start an EdTech company one day that creates video games and other media for learning STEM disciplines.

Bulhwi Cha said:

As I said in my introduction, I aim to develop games for mathematics education and study symplectic geometry so I can formalize them.

[Bulhwi Cha]

Kyle Miller said:

Regarding forks, while it's not illegal to make a fork, from a social perspective it's a last course of action, signaling that working together is impossible, and it's better to make a separate project. That's unless your 'fork' is actually just a copy where you'll do development that you intend to contribute (like Github's use of 'fork'), rather than a separate project that you intend to advertise and have compete with the original.

#tpil hasn't been actively maintained, after all. I plan to remove the parts related to mdBook from my fork. I might use Sphinx instead.

Quotes

David Thrane Christiansen said:

The work that I'm putting into it right now is quite limited, and mostly consists of merging PRs that fix very simple things, like typos, and making the code examples work in newer Lean 4 releases. I don't presently have plans to embark on any major revisions, or to make substantial changes to the text. I may also port the contents to Verso once it's mature for this use case once we get real benefits from the port (e.g. more reliable cross-linking of documents, or better dogfood-style testing of the tool).

Bulhwi Cha said:

From #tpil's README.md:

This manual is generated by mdBook. We are currently using a fork of it for the following additional features:

I think the fork is too old.

Bulhwi Cha said:

Sphinx uses gettext to generate PO files that can be translated into languages other than English. David Thrane Christiansen I wonder if Verso will also use localization tools like gettext or Fluent to support internationalization.

Related topic: #lean4 > Internationalization

[Bulhwi Cha]

Mario Carneiro said:

Joe Hendrix said:

Are there problems with that PR that I should be aware of?

I see that you made simp much more aggressively classical than before, making use of Classical.foo lemmas even when Decidable.foo lemmas could be used to similar effect (such that classical simping can be controlled by open Classical). This makes me sad, I was trying to avoid that, but I'm not really able to keep arguing on this point.

(what's worse, making them global simps in core means no one can override it in downstream projects without local un-simp-ing every time)

@Kyle Miller This decision by the core team makes it harder for people to use Lean for projects based on constructive logic. Likewise, the decision by the fictional Bean maintainer (Bulhwi 2077) to provide all documentation for the Bean project exclusively in Korean makes it harder for people who don't know Korean to use Bean.

Quote

Bulhwi Cha said:

If we follow Leo's logic in the above quote, I can create the following scenario:

In 2077, Bulhwi launched the Bean project, his fork of Lean. Since almost every Bean user is Korean, he wrote all documentation for Bean exclusively in Korean. One day, Vee, an English speaker, asked Bulhwi to translate Bean's documentation into English, but he declined. Bulhwi said, "Vee, I've talked to many Bean users, and the vast majority don't care about English translation. I've asked about high-impact projects whose developers are struggling due to lack of English documentation, and I've never got a convincing answer."

[Bulhwi Cha]

Kyle Miller said:

Regarding your Korean/English analogy, I see that as being a very different situation. People who do constructive mathematics can read and understand classical mathematics, and vice versa. In ITP communities, constructivists are very well represented, and compared to the number of constructivists in both computer science and mathematics, they are overrepresented, which is to say, despite what you hear, it's a relatively niche requirement. Lean not putting engineering effort into supporting constructivism is not stopping anyone from developing its "killer app", when there's Coq and Agda.

So, I think you're missing the gist of my analogy.

[Bulhwi Cha]

Bulhwi Cha said:

Henrik Böving Do you think the following statement isn't true? "The Bean project supports documentation exclusively in Korean."

You (Vee) can very much teach yourself Korean and translate the documentation into English without the maintainer's help; he isn't stopping you from doing this. It's just that the documentation he provided is written only in Korean, even if there are scenarios where a few English-speaking Bean users couldn't read it. But if you have a use case for that beyond "it's possible, so let's do it," I'm sure the maintainer would listen to you and re-evaluate the current (2077) stance. As Bean's maintainer explained in the above quote, the issue is that he's not been presented with such a use case yet.

[Bulhwi Cha]

I'm thinking about translating the text in my fork of #tpil into Korean. I'm not stopping anyone from translating the original text into Korean, although few Koreans are actively using Lean.

[Bulhwi Cha]

Kyle Miller said:

If you think TPIL is intentionally misleading you somehow, know it's an old document that goes back to the old days of Lean, and Lean has changed. And, overall, recently there hasn't been much energy put into updating documentation, vs put into improving Lean.

If I were a member of the Lean core team, I would've already apologized for not correcting the misleading explanation of Lean core in #tpil sooner. But it's okay. I have my fork now.

[Bulhwi Cha]

Bulhwi Cha said:

Drew Devault said:

As a contributor, you should evaluate the value system of the leadership and make a personal determination as to whether or not it aligns with your own. If it does, participate. If it does not, find an alternative or fork the project.

Forcing a project leader to make a decision they don't want is unnecessarily antagonistic. Forking the project isn't. Rather, it's a reasonable resolution of a disagreement.

@Johan Commelin As I've said earlier, anyone is welcome to suggest improvements to my PR and fork.

[Johan Commelin]

I'm not flagging the fact that you forked. But that you are blaming the Lean core team for something in #tpil even if that isn't a project ran by the Lean core team.

And I'm flagging the fact that in general the tone of your message(s) is on the unfriendly side of the spectrum (imho).

[Bulhwi Cha]

Johan Commelin said:

I'm not flagging the fact that you forked. But that you are blaming the Lean core team for something in #tpil even if that isn't a project ran by the Lean core team.

From https://lean-lang.org/documentation:

Theorem Proving in Lean 4 is the standard reference for learning how to use Lean as a theorem prover.

Quote

Eric Wieser said:

TPIL isn't (currently) owned by the FRO, right? (not that I'm saying it would be a problem if it were)

[Bulhwi Cha]

Then I hope they clarify on their website that #tpil isn't a project run by them.

[Bulhwi Cha]

Johan Commelin said:

And I'm flagging the fact that in general the tone of your message(s) is on the unfriendly side of the spectrum (imho).

I'll stop here.

[Jeremy Avigad]

@Bulhwi Cha Kyle is right -- the sentences were written almost a decade ago and need to be updated. I am sorry the upset you. We will revise them soon.

[Bulhwi Cha]

Thank you, Jeremy Avigad.

[Bulhwi Cha]

I closed the PR.

[Bulhwi Cha]

I'll reset my fork soon. I reverted the commits I made to my fork.

[Shreyas Srinivas]

@Mario Carneiro : Fully support your stance about not getting in the way of extensibility in general, but in your example of deep embeddings, wouldn't it be usual to define one's own variant of the Prop type for the type system or logic you are embedding. From what I know, existing tactics work assuming they are dealing with Prop, and these tactics would have to be rewritten anyway. So simp implicitly using classical axioms might not matter right? I have Iris's iProp in mind.

[Mario Carneiro]

Yes, for deep embeddings you can generally use tactics from lean freely in the metalogic, and they won't be applicable at all in the logic itself. The main place where you will be hampered by unnecessary axiom use in lean tactics is if your embedding system includes a mechanism for reflecting proofs proved "plainly" in lean to embedded proofs, since in that case you will be dependent on the original proofs being relatively clean and not using things outside whatever the supported subset is

[Bulhwi Cha]

Mario Carneiro said:

I keep looking for HoTT enthusiasts willing to do HoTT metatheory in mathlib because I think this is the true way forward for HoTT in lean, not changing the base axioms

What would be the motive for developing the metatheory of HoTT in Lean and Mathlib? Wouldn't HoTT enthusiasts choose other proof assistants to do it?

[Mario Carneiro]

While there are purpose-built proof assistants for synthetic homotopy theory (i.e. no "meta-") that can certainly do better than lean, I don't think there are category theory libraries that definitively outpace mathlib's, especially if you want to connect the results to other areas outside category theory like algebraic geometry or homotopy theory. Lean mathlib seems well placed to be able to simultaneously talk about all of these aspects to do HoTT metatheory, while still being flexible enough to define a competent HoTT mode (in user space).

In related news, this idea is making some actual headway here in Bonn, Steve Awodey, @Sina H 𓃵 and I have been working together on first steps toward a HoTT model in lean, although I think it's still a bit too early to say whether it will really work.

[Bulhwi Cha]

Jeremy Avigad said:

Bulhwi Cha Kyle is right -- the sentences were written almost a decade ago and need to be updated. I am sorry the upset you. We will revise them soon.

Jeremy Avigad's pull request hasn't been merged for over a month, so I reapplied my commits to my fork. But this time I also removed the phrases that many members of this community regarded as "unnecessarily antagonistic."

From https://git.sr.ht/~chabulhwi/theorem_proving_in_lean4/commit/6464a84d4e61b50b27534167cf373599a3b099e9:

M axioms_and_computation.md => axioms_and_computation.md

 However, the developers of Lean's core library currently do not want to
-implement these tactics themselves, nor do they accept any changes that
+implement these tactics themselves, nor do they accept changes that
 attempt to modify the tactics in the core to avoid using classical
-reasoning, regardless of how simple the change may be.
+reasoning.