Zulip Chat Archive

Stream: general

Topic: Implementation of Schaunel's Conjecture in Lean?

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: Dec 20 2023 at 11:08 UTC