Zulip Chat Archive

Stream: maths

Topic: Bourbaki's tau


view this post on Zulip Hamza Maimoune (Mar 26 2020 at 17:22):

Hello, I am now reading Bourbaki and I'm wondering how would the tau be represented in Lean? Thank you!

view this post on Zulip Reid Barton (Mar 26 2020 at 17:25):

probably classical.some or classical.epsilon, though this question may be too low-level to be meaningful

view this post on Zulip Patrick Massot (Mar 26 2020 at 17:29):

I think reading that part of Bourbaki is a bad idea. My understanding is that Bourbaki messed up foundations. They had no expert in this topic and, contrary to what they sort of claim, they didn't really care about foundations.

view this post on Zulip Patrick Massot (Mar 26 2020 at 17:30):

Maybe I should expand a bit on Reid's answer too: he says those τ\tau or ε\varepsilon things are too close to the logical foundations that it makes sense to compare them across very different foundational systems.

view this post on Zulip Reid Barton (Mar 26 2020 at 17:30):

At least, don't take it too seriously. Lean is not based on set theory anyways.

view this post on Zulip Hamza Maimoune (Mar 26 2020 at 17:31):

Yes, I was warned I'm just trying to traduce it into Lean as an exercise.

view this post on Zulip Reid Barton (Mar 26 2020 at 17:33):

I think this will probably make you frustrated with both Bourbaki and Lean, but up to you.

view this post on Zulip Reid Barton (Mar 26 2020 at 17:37):

(I've also never read this part of Bourbaki, so I don't really know what I am talking about.)

view this post on Zulip Hamza Maimoune (Mar 26 2020 at 17:40):

I really think that I should stop. But do you know what Bourbaki volume are interesting to read? Because I would not want to learn non standard things!

view this post on Zulip Reid Barton (Mar 26 2020 at 17:45):

Patrick could give you a better answer, but approximately: the other ones.

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 18:04):

Lie algebras and Lie groups

view this post on Zulip Kevin Buzzard (Mar 26 2020 at 18:05):

We have very little on them. I bet Lie algebras would be an interesting way to learn Lean

view this post on Zulip Patrick Massot (Mar 26 2020 at 20:09):

The stuff in general topology is slightly non-standard, but excellent. Basically it's non-standard only because people usually don't bother to provide proofs. It's 100% standard in proof assistants.

view this post on Zulip Hamza Maimoune (Mar 26 2020 at 20:16):

Thank you!


Last updated: May 14 2021 at 18:28 UTC