Dedekind Numbers Closed Form

[aryanamol10]

-Fixed docstring to accurately represent situation and conform with formalization logic

[mo271]

Thanks, I guess as with many non-Prop valued answer(sorry) it will be up to the reader to see if the answer is useful.

I think it would be nice to actually add the formula from the wikipedia, that would explain more more clearly what what is meaant"logical closed-form summation exists".
Also, this comes from the wikipedia sentence "no closed-form expression for $M(n)$ is known" and I suppose we don't care much about "computationally efficient", which is another angle to it. One could image something that is computationally efficient but not a closed form.

[aryanamol10]

Hey @mo271, thank you for the advice and feedback.

I’ve drafted a set of edits to address the misformalization by aligning the file with the existing literature and the concerns raised here:

Explicit Formula: I added the Kisielewicz summation formula directly to the theorem. This provides clarity on what is meant by a 'logical closed form' and serves as a better reference than a vague placeholder.

Docstring Alignment: I updated the docstring to match the Wikipedia/mathematical consensus: 'No simple or computationally efficient closed-form expression for M(n) is known.' This removes the contradictory double-negative in the original file.

Refining 'Efficiency' vs. 'Form': I added a note to distinguish between the existence of a closed-form summation and the ongoing research frontier of computational efficiency (e.g., finding M(10)).

Hopefully, these edits clarify the status of the Dedekind numbers and resolve the usefulness issue for the reader.

[franzhusch]

Thanks, I guess as with many non-Prop valued answer(sorry) it will be up to the reader to see if the answer is useful.

I think it would be nice to actually add the formula from the wikipedia, that would explain more more clearly what what is meaant"logical closed-form summation exists". Also, this comes from the wikipedia sentence "no closed-form expression for M ( n ) is known" and I suppose we don't care much about "computationally efficient", which is another angle to it. One could image something that is computationally efficient but not a closed form.

I feel like it is somewhat philosophical what a "closed-form" is. If one uses mathematical notation as programming and invents more mathematical notation, then one can probably find a closed-form for almost anything. This being said a notion of efficient "closed-form" is probably what most would consider a closed-form or a "closed-form", which gives more insights into the structure of the object.

Edit: I did not know, that "closed-form" has a precise technical definition. So my above paragraph mostly refers to mathematical expression then I suppose. But the question on the computational complexity of different closed-form expressions remains.

I would actually want something akin to a answerNumeral(sorry), which takes in a string of numerals, converts them to a natural number and then this natural number is proven to be equivalent to M(10). But this might be something for a separate PR and we can then use it here (and also for Ramsey Numbers for example).

[aryanamol10]

Hey @franzhusch, just wanted to confirm, are we addressing the answerNumeral(sorry) and nuanced "closed-form" logic in this PR or for future implementations?

This way I can make necessary changes on docstring if we need to apply.