Vaibhav Karve prerecorded talks

Stream: Lean Together 2021

[Rob Lewis]

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]

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]

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

[Aaron Anderson]

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]

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]

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]

@Vaibhav Karve very interesting!

[Vaibhav Karve]

@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.