Luigi Massacci

Stream: new members

[Luigi Massacci]

Hello everyone!

I’m a Math & Comp. Sci. undergraduate at École polytechnique. I discovered Lean thanks to the Natural Numbers game (which is awesome by the way), and then did an internship last summer automatically extracting lean proofs from a graphical proof assistant for first order logic.

I moved on to Coq this past year to do more TCS related formalizations, but now I’d like to do some “real” math with Lean, hopefully contributing to mathlib in the future. I’m also interested in the tactics side of things.

Cheers :tada:

[Johan Commelin]

Welcome! Which graphical proof assistant was that? Is your work available somewhere online?

[Luigi Massacci]

Hello, the proof assistant, which is based on linking, can be played with here, including the extraction to lean3 and 4. I don't think there's anything online as to how that works under the hood, yet.