Andreas Gittis

Stream: new members

[Andreas Gittis]

Hi everyone,

I'm a computer science PhD student at UC Santa Cruz. I've just started an automated theorem proving project and I'm going to be trying to use mathlib and Lean 4. I'm relatively new to the language, especially the metaprogramming side. I had a great time with the Theorem Proving in Lean book; thank you to the authors and everyone else who helped put it together. I'm looking forward to learning more about Lean in the coming months; hopefully I do not deluge everyone here with too many bothersome questions. Cheers.

[Floris van Doorn]

I hope you've also found the metaprogramming book: https://github.com/arthurpaulino/lean4-metaprogramming-book

[Mauricio Collares]

Oooh, I just noticed the metaprogramming book is available as a PDF! Much appreciated.

[Andreas Gittis]

Floris van Doorn said:

I hope you've also found the metaprogramming book: https://github.com/arthurpaulino/lean4-metaprogramming-book

Yes I have, thanks.