Ingmar Velien (Apr 16 2022 at 12:51):
Is Schanuel's Conjecture already implemented in Lean?
If yes, where?
If not, how could we do that?
Yaël Dillies (Apr 16 2022 at 13:34):
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 (Apr 16 2022 at 14:34):
@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 (Apr 16 2022 at 17:56):
At the moment, I would like to leave that to the more experienced.
Ingmar Velien (May 15 2022 at 15:31):
Now I'm ripe to get a hint. How could we formulate Schanuel's conjecture in Lean?
Last updated: Aug 03 2023 at 10:10 UTC