Simon Guilloud

Stream: new members

[Simon Guilloud]

Hi everyone!
I am a PhD student from EPFL (graduating soon, hopefully), with a background in verification, logic and ITPs. I led the development of a home made/experimental proof assistant, and hope to learn some more Lean and try to contribute to mathlib.

I aim for developing the theory of ortholattices, which I believe are not defined in mathlib, and in particular the decidability of the word problem for ortholattices (and incidentally for lattices) which I have already formalized in Rocq. At the moment I am a bit lost in the jungle of type classes in the theory of orders and lattices and the various ways they are defined, so I'll just read the Lean references for a little while and then probably will ask a few questions!

Bests,

Simon

[(deleted)]

What's your proof assistant

[Simon Guilloud]

It is called "Lisa" and is based on set theory. Of course it is incomparable in its development to Lean. It looks like this in practice:
[https://github.com/epfl-lara/lisa/blob/main/lisa-sets/src/main/scala/lisa/maths/SetTheory/Order/WellOrders/WellOrder.scala]