Lean[1] Zulip chat[2]
[1] https://leanprover-community.github.io/ [2] https://leanprover.zulipchat.com/
Readit NewsIf I’m not mistaken, this is the first use of a proof assistant to settle the status of a difficult proof that had been sitting in limbo for years. There were some previous projects (e.g. the Four Color Theorem in Coq) that validated existing proofs with a large computational element handled by untrusted software, but I think this is the first one where the epistemological status of the result was uncertain in the larger mathematical community.
Liquid Tensor Experiment also comes to mind:
https://www.nature.com/articles/d41586-021-01627-2
https://leanprover-community.github.io/blog/posts/lte-final/
I tried Lean twice and what caused me to stop both times was a severe lack of documentation. That's a shame, because it's an awesome language.
Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment.
Is Lean a Category?
(like much debated: is Hask(ell) a Category)
"In this section we set up the theory so that Lean's types and functions between them can be viewed as a `LargeCategory` in our framework."
So it seems to be proven that there is a Category Lean!
https://github.com/leanprover-community/mathlib4/blob/master...
Yes for the fragment of total and noncomputable functions which mathematicians use. For partial functions (which Lean also supports) I think the same arguments hold as for the "Haskell Category".
Though I did not find Topos Theory.
There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2]
[1] https://github.com/leanprover-community/mathlib4/tree/master...
[2] https://leanprover-community.github.io/blog/posts/lte-final/
Deleted Comment
hiker commented on Linear Address Spaces: Unsafe at any speed queue.acm.org/detail.cfm?... · Posted by u/g0xA52A2A
hiker commented on Functors and Monads for People Who Have Read Too Many “Tutorials” jerf.org/iri/post/2958... · Posted by u/zdw
Because most people suck at taking abstract mathematical concepts and seeing how they could apply to code. Including me. Let's take the definition of a function:
> A function is a relation for which each value from the set the first components of the ordered pairs is associated with exactly one value from the set of second components of the ordered pair.
Cool, I have no idea what the fuck this means and how it is useful to me.
Oh wait, I use them every day.
> Cool, I have no idea what the fuck this means and how it is useful to me.
> Oh wait, I use them every day.
Do you really? Do the `functions` you use even fit the above definition?
I bet you can think of infinite number of functions (bool -> bool). The above definition admits only 4 such functions.
hiker commented on Functors and Monads for People Who Have Read Too Many “Tutorials” jerf.org/iri/post/2958... · Posted by u/zdw
Do you happen to know of any programming language which has explicit support for multiple categories?
Lean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes.
[0] https://leanprover.github.io/programming_in_lean/#01_Introdu...
[1] https://github.com/leanprover-community/mathlib/blob/master/...
https://history-computer.com/software/simula-guide/
Thus, while I had thought Lisp had ADT concepts before the first OOL existed, now I am not sure. My remark that they originated in Lisp had been said with the intention that I was talking about the first language to have it. The idea that the concept had been described outside of an actual language is tangential to what I had intended to say, which is news to me. Thanks for the link.
https://dl.acm.org/doi/pdf/10.1145/366199.366256
and the paper even starts with a critique of the efficiency of Lisp's approach for representing data with cons pairs (citing McCarthy's paper from the same year).
You might also want to watch Casey's great talk on the history of OOP
https://www.youtube.com/watch?v=wo84LFzx5nI