Zulip Chat Archive

Stream: general

Topic: Nantes talk video


view this post on Zulip Patrick Massot (Jan 18 2019 at 11:52):

The maths department in Nantes uploaded the video of the Lean talk I gave in November at http://media.math.sciences.univ-nantes.fr/fr/node/801 It's in French and the most interesting part was also in my Amsterdam talk, but it could still be useful for people who intend to give talks presenting Lean to mathematicians.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 12:27):

Thanks a lot for posting this Patrick. I hope to be finding myself in this sort of position many times in the future.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 17:47):

I'm watching this video now. After you typed split in the function proof, how did you get { sorry} x 2 to appear instantly?

view this post on Zulip Patrick Massot (Jan 18 2019 at 17:50):

User code snippet

view this post on Zulip Patrick Massot (Jan 18 2019 at 17:51):

In my ~/.config/Code/User/snippets/lean.json I see:

view this post on Zulip Patrick Massot (Jan 18 2019 at 17:51):

"Split": {
        "prefix": "split",
        "body": [
          "split,",
          "{ $0",
          "  sorry },",
          "{ ",
          "  sorry },"
        ],
        "description": "Split tactic"
        },

view this post on Zulip Patrick Massot (Jan 18 2019 at 17:52):

Do you understand enough French to understand me, or are following only through Lean?

view this post on Zulip Johan Commelin (Jan 18 2019 at 17:56):

Kevin gave math talks in French!

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:06):

My French is good enough to understand what you're saying. The camera is off now though -- in your group theory proof I can't see the first four or five characters of every line in the VS Code.

view this post on Zulip Patrick Massot (Jan 18 2019 at 18:07):

I forgot, you can talk about "une groupe"!

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:08):

:-/


Last updated: May 11 2021 at 21:10 UTC