Zulip Chat Archive

Stream: Lean Together 2021

Topic: Vaibhav Karve prerecorded talks

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!

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:

Aaron Anderson (Jan 05 2021 at 23:52):

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

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.

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)

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.

Adam Topaz (Jan 06 2021 at 00:12):

@Vaibhav Karve very interesting!

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: Dec 20 2023 at 11:08 UTC