Zulip Chat Archive

Stream: Lean Together 2021

Topic: Vaibhav Karve prerecorded talks


view this post on Zulip Rob Lewis (Jan 05 2021 at 16:07):

Vaibhav has contributed two prerecorded talks: Axiomatic Geometry in Lean and Model Theory in Lean. These will become YouTube links when I have time, but we wanted to make them available ASAP. Ask him questions at tomorrow's social session!

view this post on Zulip Vaibhav Karve (Jan 05 2021 at 16:39):

Rob & Patrick, thank you once again for opportunity to speak! I am loving the conference. The only thing missing is the Pittsburg weather from last time :smile: :snowflake:

view this post on Zulip Aaron Anderson (Jan 05 2021 at 23:52):

I'm excited to see more model theory being done!

view this post on Zulip Aaron Anderson (Jan 05 2021 at 23:55):

I certainly find this definition of terms easier to read than the Flypitch definition - but without having worked in detail with either, I'm not sure what the technical advantages of one over the other are.

view this post on Zulip Aaron Anderson (Jan 06 2021 at 00:03):

Also - @Vaibhav Karve, you mentioned avoiding fin n because the API is tricky. Are you aware of @Reid Barton's finvec PR? (#4406)

view this post on Zulip Aaron Anderson (Jan 06 2021 at 00:04):

Perhaps a more robust finvec API would help - or maybe it'd just have the same nested inductive type issue as using vector, I'm not sure.

view this post on Zulip Adam Topaz (Jan 06 2021 at 00:12):

@Vaibhav Karve very interesting!

view this post on Zulip Vaibhav Karve (Jan 06 2021 at 14:03):

@Aaron Anderson I had not seen that PR. Thanks for pointing that out. @Gabriel Ebner pointed out in one of the comments on that PR that finvec will not result in nested induction. :tada: However, we will still need a strong API for finvec in order to make it work.


Last updated: May 08 2021 at 22:13 UTC