Conversation

Notices

1. Embed this notice
   バツ子（ラブと小雨 (shmibs@tomo.airen-no-jikken.icu)'s status on Saturday, 15-Oct-2022 02:26:38 JST バツ子（ラブと小雨
   
   mpv-shot0001.png
   • Embed this notice
     バツ子（ラブと小雨 (shmibs@tomo.airen-no-jikken.icu)'s status on Saturday, 15-Oct-2022 02:38:56 JST バツ子（ラブと小雨

     in reply to

     • JyatiriJygalo
     @placholdr
     was watching avigad's things because his new book came out (logic). and this was same channel as one, lectures for that applied category theory book from a few years ago that's gotten so popular, so looking
   • Embed this notice
     JyatiriJygalo (placholdr@pl.nulled.red)'s status on Saturday, 15-Oct-2022 02:38:57 JST JyatiriJygalo

     in reply to
     @shmibs you learning real analysis?
   • Embed this notice
     バツ子（ラブと小雨 (shmibs@tomo.airen-no-jikken.icu)'s status on Saturday, 15-Oct-2022 02:43:50 JST バツ子（ラブと小雨

     in reply to

     • JyatiriJygalo
     @placholdr
     book 1:
     https://www.cambridge.org/us/academic/subjects/mathematics/logic-categories-and-sets/mathematical-logic-and-computation
     (he does proof assistant work, including lean stuff recently with that buzzard
     
     book 2:
     https://www.cambridge.org/us/academic/subjects/mathematics/logic-categories-and-sets/invitation-applied-category-theory-seven-sketches-compositionality
     
     lectures:
     https://www.youtube.com/playlist?list=PLhgq-BqyZ7i5lOqOqqRiS0U5SwTmPpHQ5
   • Embed this notice
     JyatiriJygalo (placholdr@pl.nulled.red)'s status on Saturday, 15-Oct-2022 02:43:51 JST JyatiriJygalo

     in reply to
     @shmibs links?
   • Embed this notice
     バツ子（ラブと小雨 (shmibs@tomo.airen-no-jikken.icu)'s status on Saturday, 15-Oct-2022 02:44:35 JST バツ子（ラブと小雨

     in reply to

     • JyatiriJygalo
     @placholdr
     https://leanprover-community.github.io/mathematics_in_lean/
   • Embed this notice
     バツ子（ラブと小雨 (shmibs@tomo.airen-no-jikken.icu)'s status on Saturday, 15-Oct-2022 03:06:55 JST バツ子（ラブと小雨

     in reply to

     • JyatiriJygalo
     • fiat volvntas tva
     @placholdr @scathach
     not sure how you mean. it's a funclang to be used as an interactive proof assistant for implementing maths rigorously, so findings can be computer-verified. maybe there's some syntactic similarity? haven't used here lean before yet, so can't comment much more on except there's been some adoption from "real mathematicians" compared to other systems, which is kind of exciting
   • Embed this notice
     JyatiriJygalo (placholdr@pl.nulled.red)'s status on Saturday, 15-Oct-2022 03:06:56 JST JyatiriJygalo

     in reply to

     • fiat volvntas tva
     @shmibs I just skimmed a tiny bit so I might be wrong but isn't this just M-expressions?
     @scathach