Mathieu Guay-Paquet (introduction)

Stream: new members

[Mathieu Guay-Paquet]

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]

Also, I have a recent blog post about Props and Types in Lean, if anyone is curious.

[Jeremy Avigad]

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]

Mathieu Guay-Paquet said:

Also, I have a recent blog post about Props and Types 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]

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