Angelo Lucia

Stream: new members

[Angelo Lucia]

Hello all,

my name is Angelo, and I am a mathematician at Universidad Complutense de Madrid in Spain. In the last months I got interested in Lean for formalizing math proofs, and after doing some of the math-oriented tutorials I decided I wanted to try writing some stuff myself and maybe contribute to Mathlib if I can.

My area of expertise is mathematical physics (quantum spin and quantum information), but I do have a side interest in graph theory (and I did some work on chromatic polynomials), so I was hoping to start from there.

I am glad to be here, and I hope to learn from what it seems to be a very nice and active community!

[Kevin Buzzard]

One way to find a project is to start with a random basic theorem about eg chromatic polynomials and challenge yourself to formalise it. Clone mathlib and work in that repo in a scratch file and see how far you get! Ask in #new members if you're stuck. Formalisation is harder than it looks but very satisfying when it works :-)

[Frédéric Dupuis]

Hi! Always nice to see another quantum information theorist here! There's quite a bit going on in operator algebras also (see the Mathlib.Analysis.CstarAlgebra folder for example) that you might be interested in. I really to hope to be able to start formalizing the sort of work we do in the medium term!

[Alex Meiburg]

Hi! :) Yay, more of us!

I've written down some quantum info topics in a repo at https://github.com/Timeroot/Lean-QuantumInfo/, you might want to look. So far it's oriented pretty exclusively to finite dimensional stuff, and full of sorrys. See e.g. https://github.com/Timeroot/Lean-QuantumInfo/blob/main/QuantumInfo/Finite/CPTPMap.lean