Nantes talk video

Stream: general

[Patrick Massot]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

User code snippet

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

Kevin gave math talks in French!

[Kevin Buzzard]

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.

[Patrick Massot]

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

[Kevin Buzzard]

:-/