# Zulip Chat Archive

## Stream: new members

### Topic: Mathieu Guay-Paquet (introduction)

#### Mathieu Guay-Paquet (May 04 2020 at 21:07):

Hi! I was in math academia for a few years, then I left for industry for a few years, and now I'm hovering in-between. I'd like to consider myself both a real mathematician and a computer scientist, and it makes me sad that we often talk about these two groups as opposites, even though I can tell when I'm being more mathy or more programmy.

Some of my favourite math things are representations of the symmetric group, symmetric functions, graded Hopf algebras, formal power series, combinatorial algorithms, and bijective proofs. My hope with Lean (and/or other systems) is to formalize the recent research (including my own) on the combinatorics of Hessenberg varieties, because there are enough implicit, fiddly, tedious bits in there that I don't fully trust humans (including me) to check everything.

#### Mathieu Guay-Paquet (May 04 2020 at 21:10):

Also, I have a recent blog post about `Prop`

s and `Type`

s in Lean, if anyone is curious.

#### Jeremy Avigad (May 04 2020 at 21:33):

Welcome Mathieu! One of my favorite things about interactive theorem proving is that it gets mathematicians and computer scientists talking to each other (in a good way).

#### Matt Earnshaw (May 05 2020 at 16:30):

Mathieu Guay-Paquet said:

Also, I have a recent blog post about

`Prop`

s and`Type`

s in Lean, if anyone is curious.

welcome & nice post! it is perhaps worth mentioning that we can also use choice to give `classical.choice ∘ look_at_this_one : pretty -> flower`

, but then we cannot compute with the data so produced

#### Mathieu Guay-Paquet (May 05 2020 at 19:27):

@Matt Earnshaw good point! I may add axioms as a way to go from Props to Types, such as `classical.choice`

Last updated: May 06 2021 at 22:13 UTC