New member introduction

Stream: new members

[Lorenzo Saraiva]

Hello everyone! My name is Lorenzo Saraiva. I am currently pursuing my PhD in PUC-Rio, Brazil, and I'm working in the formalization of tree-like compressed Natural Deduction proofs in minimal implicational logic as boolean circuits in Lean. This is extending upon the work by my advisor, E. H. Haeusler and by L. Gordeev.

Working with Lean has been quite challenging but rewarding, I had just a small background in Coq before starting with this. After a lot of work I finally reached what I like to believe is a milestone in the development.

So hello again everyone, I look forward to working with you! I will link my repo with the complete lean file (I'm not sure this is the correct way to share lean code here, correct me if I'm wrong). I'd be very happy with any reviews, suggestions o critics! I suspect I might have several places where I could have used an existing resource, or done things a bit simpler.

Thank you for you attention and hope to learn a lot here!

https://github.com/lorenzosaraiva/DLDSBooleanCircuit