Implementation of Schaunel's Conjecture in Lean?

Stream: general

[Ingmar Velien]

Is Schanuel's Conjecture already implemented in Lean?

If yes, where?

If not, how could we do that?

[Yaël Dillies]

We currently do not really state conjectures in mathlib. There is however discussion about it. See for example https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/conjecture.20declaration

[Johan Commelin]

@Ingmar Velien I'm not aware of a Lean formalisation of the statement. But this shouldn't be hard. Do you want to try? Or do you want a hint?

[Ingmar Velien]

At the moment, I would like to leave that to the more experienced.

[Ingmar Velien]

Now I'm ripe to get a hint. How could we formulate Schanuel's conjecture in Lean?