<div dir="ltr"><div dir="ltr"><div>Hey Thorsten,</div><div><br></div></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 12 Mar 2020 at 15:36, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">[snip] <br></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">This is a shame because in many ways lean is a nice system but it is unusable if you want to do structural Mathematics.<br></blockquote><div><br></div><div>I do not recognise your objection. I agree that equality between types is an issue in Lean. What I do not understand is why this matters to mathematicians in practice. Since "working mathematicians" became involved with using Lean the collection of mathematical structures formalised in Lean and theorems about these structures has gone through the roof. Lean as a powerful and exponentially growing classical mathematical library, which covers essentially all of a first year undergraduate mathematics curriculum and is well over half way through the second year, as well as being much more advanced (MSc level) in other areas such as algebra. Maybe I just don't know what "structural mathematics" is, but Lean is certainly usable if you want to do the kind of mathematics which is actually happening in mathematics departments. I am hopeful that one day this will happen with one of the HoTT systems but at the minute the only areas where they appear to go deep are synthetic homotopy theory and category theory, topos theory, abstract higher category theory etc. I have this nagging worry that away from these areas the univalence axiom (and the way it seems to rule out Lean's powerful impredicative Prop and a useful equality taking values in that Prop) is more than a hindrance than a help. But I would love to be proved wrong. One thing that absolutely needs emphasizing is that classical logic is absolutely embedded in an undergraduate mathematics degree nowadays, and no "working mathematician" will take you seriously if you try to remove it. This is apparently an uncomfortable fact for some in the community but it is one which I think it is important to remind people of; mathematics departments went classical in several central areas, many many decades ago, and we are not going back. Yes I know the proof of the odd order theorem is constructive. And we don't care. This is a statement about finite objects and unrepresentative of what is actually happening in 2020.<br></div><div><br></div><div>I think that Isabelle/HOL and HOL Light are evidence that for lots of mathematics (especially much of 19th and early 20th century mathematics) one does not even need dependent types, but I have this idea (again which I would love to be wrong about) suggesting that MSc level algebraic geometry and homological algebra are just too inconvenient to use without dependent types. In Lean we are moving onto Ext and Tor in the category of R-modules. I think it would be an extremely interesting project to see how these worked in practice in other systems. <br></div><div><br></div><div>Going further -- what is absolutely clear is that to get a better understanding of what the truth actually is, regarding the difficulty formalising the actual mathematics going on in mathematics departments in central areas such as algebra, geometry, number theory, analysis etc, we need *actual data*. We need libraries which correspond to what is being taught in mainstream undergraduate mathematics courses, in all the systems, if we want to see what the actual truth is. Sure every undergraduate pure maths course can be formalised in every system, in theory. But can it be formalised in finite time in a usable way in practice? This is what we simply do not know and I believe that we can only find out by getting more working mathematicians on board.<br></div><div><br></div><div>An interesting test with Lean will be what happens when Lean 4 is released. Lean 4 will not be backwards compatible with Lean 3 so the library will have to be ported from scratch, and it's got pretty big. The underlying type theory is not changing but the type class inference system is changing completely, and typeclasses are everywhere in Lean's maths library.</div><div><br></div><div>I should finish by taking the time to advertise Gabriel Ebner's HoTT library in Lean 3: <a href="https://github.com/gebner/hott3">https://github.com/gebner/hott3</a> . It adds a [hott] attribute to the system and "disables" singleton elimination. What can one do with it? Nobody really knows. Maybe for you (Thorsten) it's the best of both worlds?<br></div><div><br></div><div>Kevin<br></div><div><br></div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
Thorsten<br>
<br>
On 08/03/2020, 14:25, "Agda on behalf of Bas Spitters" <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a> on behalf of <a href="mailto:b.a.w.spitters@gmail.com" target="_blank">b.a.w.spitters@gmail.com</a>> wrote:<br>
<br>
Dear Kevin,<br>
<br>
The excitement about HoTT is that it has brought together several<br>
communities. Some are interested in homotopy theory and higher<br>
category theory, some (like Vladimir) want a new foundation for modern<br>
mathematics.<br>
Some combine those two by higher toposes.<br>
<br>
Some are trying to improve the previous generation of proof<br>
assistants. E.g. this influenced the design of quotients types in<br>
lean.<br>
By Curry-Howard this also influences the design of programming<br>
languages, like the cubical agda programming language<br>
(<a href="https://pure.itu.dk/portal/files/84649948/icfp19main_p164_p.pdf" rel="noreferrer" target="_blank">https://pure.itu.dk/portal/files/84649948/icfp19main_p164_p.pdf</a>)<br>
<br>
If we consider HoTT as an extension of type theory with the univalence<br>
axiom, then *of course* everything that was done before can still be<br>
done.<br>
E.g. the proof of Feit-Thompson is constructive and thus also works in<br>
HoTT. (I can elaborate on this if needed.)<br>
<br>
In fact, classical logic is valid in the simplicial set model<br>
(<a href="https://www.math.uwo.ca/faculty/kapulkin/notes/LEM_in_sSet.pdf" rel="noreferrer" target="_blank">https://www.math.uwo.ca/faculty/kapulkin/notes/LEM_in_sSet.pdf</a>).<br>
Moreover, that model also interprets strict propositions, so one could<br>
even extend lean with univalence (I believe).<br>
It would be interesting to know whether this simplifies the definition<br>
of perfectoid spaces.<br>
<br>
Best regards,<br>
<br>
Bas<br>
<br>
On Thu, Mar 5, 2020 at 12:25 PM Kevin Buzzard <<a href="mailto:kevin.m.buzzard@gmail.com" target="_blank">kevin.m.buzzard@gmail.com</a>> wrote:<br>
><br>
><br>
><br>
> On Wed, 4 Mar 2020 at 07:18, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>> wrote:<br>
>><br>
>> Dependent types are good for pure mathematics (classical or<br>
>> constructive). They are the natural home to define group, ring, metric<br>
>> space, topological space, poset, lattice, category, etc, and study them.<br>
>> Mathematicians that use(d) dependent types include Voevodsky (in Coq)<br>
>> and Kevin Buzzard (in Lean), among others. Kevin and his team defined,<br>
>> in particular, perfectoid spaces in dependent type theory. Martin<br>
><br>
><br>
> The BCM (Buzzard, Commelin, Massot) paper defined perfectoid spaces in Lean<br>
> and looking forwards (in the sense of trying to attract "working mathematicians"<br>
> into the area of formalisation) I think it's an interesting question as to whether this definition<br>
> could be made in other systems in a way which is actually usable. My guess: I don't see why it couldn't<br>
> be done in Coq (but of course the type theories of Lean and Coq are similar), although<br>
> there is a whole bunch of noncomputable stuff embedded in the mathematics.<br>
> I *suspect* that it would be a real struggle to do it in any of the HOL systems<br>
> because a sheaf is a dependent type, but these HOL people are good at tricks<br>
> for working around these things -- personally I would start with seeing whether<br>
> one can set up a theory of sheaves of modules on a locally ringed space in a HOL<br>
> system, because that will be the first stumbling block. And as for the HoTT systems,<br>
> I have no feeling as to whether it is possible to do any serious mathematics other than<br>
> category theory and synthetic homotopy theory -- my perception is that<br>
> the user base are more interested in other kinds of questions.<br>
><br>
> In particular, connecting back to the original question, a sheaf of modules on a<br>
> locally-ringed space is a fundamental concept which shows up in a typical MSc<br>
> or early PhD level algebraic geometry course (they were in the MSc algebraic<br>
> geometry course I took), and if one wants to do this kind of mathematics in a<br>
> theorem prover (and I do, as do several other people in the Lean community)<br>
> then I *suspect* that it would be hard without dependent types. On the other hand<br>
> I would love to be proved wrong.<br>
><br>
> Kevin<br>
>><br>
>><br>
>> On 03/03/2020 19:43, <a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a> wrote:<br>
>> > I'm in the process of writing my thesis on proof assistant performance<br>
>> > bottlenecks (with a focus on Coq), and there's a large class of<br>
>> > performance bottlenecks that come from (mis)using the power of dependent<br>
>> > types. So in writing the introduction, I want to provide some<br>
>> > justification for the design decision of using dependent types, rather<br>
>> > than, say, set theory or classical logic (as in, e.g., Isabelle/HOL).<br>
>> > And the only reasons I can come up with are "it's fun" and "lots of<br>
>> > people do it"<br>
>> ><br>
>> > So I'm asking these mailing lists: why do we base proof assistants on<br>
>> > dependent type theory? What are the trade-offs involved?<br>
>> > I'm interested both in explanations and arguments given on list, as well<br>
>> > as in references to papers that discuss these sorts of choices.<br>
>> ><br>
>> > Thanks,<br>
>> > Jason<br>
>> ><br>
>> > _______________________________________________<br>
>> > Agda mailing list<br>
>> > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>> ><br>
>><br>
>> --<br>
>> Martin Escardo<br>
>> <a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
><br>
> --<br>
> You received this message because you are subscribed to the Google Groups "lean-user" group.<br>
> To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:lean-user%2Bunsubscribe@googlegroups.com" target="_blank">lean-user+unsubscribe@googlegroups.com</a>.<br>
> To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/lean-user/CAH52Xb0X%3D06U2O7K%2BLGRXyPu%3DhaKxp2FcQr3SFK0f4jm8kv9mQ%40mail.gmail.com" rel="noreferrer" target="_blank">https://groups.google.com/d/msgid/lean-user/CAH52Xb0X%3D06U2O7K%2BLGRXyPu%3DhaKxp2FcQr3SFK0f4jm8kv9mQ%40mail.gmail.com</a>.<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<br>
<br>
<br>
<br>
<br>
</blockquote></div></div>