## Stream: maths

### Topic: Bourbaki's tau

#### 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!

#### 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

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

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

#### Reid Barton (Mar 26 2020 at 17:30):

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

#### Hamza Maimoune (Mar 26 2020 at 17:31):

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

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

#### 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.)

#### 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!

#### Reid Barton (Mar 26 2020 at 17:45):

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

#### Kevin Buzzard (Mar 26 2020 at 18:04):

Lie algebras and Lie groups

#### 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

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

#### Hamza Maimoune (Mar 26 2020 at 20:16):

Thank you!

Last updated: May 14 2021 at 18:28 UTC