Lean Formalisation of constants

[felixpernegger]

Similar to the erdosproblems repository, it may be nice/useful to have links to Lean formalisations of the definitions of the various constants (+ formalised conjectures about them etc.)?
This could probably be done in the formal conjectures repository or by setting up something something new.
This potentially could also help AI tools I suppose.

[teorth]

It might be worth raising this issue at the formal conjectures repository. One issue is that we haven't quite stabilized our numbering system yet, so having a separate repository to track similar data may cause some synchronization issues.

[felixpernegger]

Posted about this on Zulip now.
https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Optimization.20constants/with/570016079

[teorth]

To try to fix the numbering system going forward, I will try to keep any number assigned to a problem static, with the single exception that I may relabel "N" to "Na" if a subsequent constant similar to "N" shows up (which would then be assigned "Nb"). So, if one adopts the convention that any constant given a numeric label "N" is secretly actually being given the label "Na" (but with the "a" being "silent") then the labels assigned will be static going forward.